diff --git a/library/init/meta/tactic.lean b/library/init/meta/tactic.lean
index 94adcc62e9..2c29168bd9 100644
--- a/library/init/meta/tactic.lean
+++ b/library/init/meta/tactic.lean
@@ -766,9 +766,9 @@ open tactic
 run_command do
  l  ← return $ level.param `l,
  Ty ← return $ expr.sort l,
- type ← to_expr `(Π {α : %%Ty}, α → α),
- val  ← to_expr `(λ {α : %%Ty} (a : α), a),
+ type ← to_expr `(Π (α : %%Ty), α → α),
+ val  ← to_expr `(λ (α : %%Ty) (a : α), a),
  add_decl (declaration.defn `id_locked [`l] type val reducibility_hints.opaque tt)
 
-lemma id_locked_eq {α : Type u} (a : α) : id_locked a = a :=
+lemma id_locked_eq {α : Type u} (a : α) : id_locked α a = a :=
 rfl
diff --git a/tests/lean/anc1.lean.expected.out b/tests/lean/anc1.lean.expected.out
index 8a83dd85a2..5996d30e91 100644
--- a/tests/lean/anc1.lean.expected.out
+++ b/tests/lean/anc1.lean.expected.out
@@ -2,7 +2,7 @@
 and.intro trivial trivial : true ∧ true
 sigma.mk 1 sorry : Σ (x : ℕ), x > 0
 show true, from true.intro : true
-Exists.intro 1 (id_locked (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
+Exists.intro 1 (id_locked (1 ≠ 0) (λ (a : 1 = 0), nat.no_confusion a)) : ∃ (x : ℕ), 1 ≠ 0
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C), show B ∧ A, from and.intro Hb Ha :
   ∀ (A B C : Prop), A → B → C → B ∧ A
 λ (A B C : Prop) (Ha : A) (Hb : B) (Hc : C),