diff --git a/tests/lean/run/elim2.lean b/tests/lean/run/elim2.lean
index 8c1c738f5..01b82c087 100644
--- a/tests/lean/run/elim2.lean
+++ b/tests/lean/run/elim2.lean
@@ -4,5 +4,5 @@ constant p : num → num → num → Prop
 axiom H1 : ∃ x y z, p x y z
 axiom H2 : ∀ {x y z : num}, p x y z → p x x x
 theorem tst : ∃ x, p x x x
-:= obtain a b c H [visible], from H1,
+:= obtain a b c H, from H1,
      by (apply exists.intro; apply H2; eassumption)