diff --git a/library/init/logic.lean b/library/init/logic.lean
index 23a777e70..b5728fefc 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -415,7 +415,7 @@ inhabited.rec H2 H1
 definition default (A : Type) [H : inhabited A] : A :=
 inhabited.rec (λa, a) H
 
-opaque definition arbitrary (A : Type) [H : inhabited A] : A :=
+definition arbitrary [irreducible] (A : Type) [H : inhabited A] : A :=
 inhabited.rec (λa, a) H
 
 definition Prop.is_inhabited [instance] : inhabited Prop :=
diff --git a/library/tools/fake_simplifier.lean b/library/tools/fake_simplifier.lean
index 4f3bf0702..ff5bf6273 100644
--- a/library/tools/fake_simplifier.lean
+++ b/library/tools/fake_simplifier.lean
@@ -3,6 +3,6 @@ open tactic
 namespace fake_simplifier
 
 -- until we have the simplifier...
-opaque definition simp : tactic := apply sorry
+definition simp : tactic := apply sorry
 
 end fake_simplifier