diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index 6639bb017d..bd347cd43b 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -192,8 +192,8 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 @[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do
   match stx with
   | `(tactic| intro)                   => introStep none `_
+  | `(tactic| intro _)                 => introStep none `_
   | `(tactic| intro $h:ident)          => introStep h h.getId
-  | `(tactic| intro _%$tk)             => introStep tk `_
   | `(tactic| intro $pat:term)         => evalTactic (← `(tactic| intro h; match h with | $pat:term => ?_; try clear h))
   | `(tactic| intro $h:term $hs:term*) => evalTactic (← `(tactic| intro $h:term; intro $hs:term*))
   | _ => throwUnsupportedSyntax
@@ -222,7 +222,8 @@ where
       return (fvars, [mvarId])
     withMainContext do
       for stx in ids, fvar in fvars do
-        Term.addLocalVarInfo stx (mkFVar fvar)
+        if stx.isIdent then
+          Term.addLocalVarInfo stx (mkFVar fvar)
   | _ => throwUnsupportedSyntax
 
 @[builtinTactic Lean.Parser.Tactic.revert] def evalRevert : Tactic := fun stx =>
diff --git a/tests/lean/1204.lean b/tests/lean/1204.lean
new file mode 100644
index 0000000000..557bc7ecef
--- /dev/null
+++ b/tests/lean/1204.lean
@@ -0,0 +1,15 @@
+theorem unused_intro: (n m: Nat) -> (m >= 0) :=
+  by
+    intro _ m; simp
+
+theorem unused_intros: (n m: Nat) -> (m >= 0) :=
+  by
+    intros _ m; simp
+
+theorem unused_intro': (n m: Nat) -> (m >= 0) :=
+  by
+    intro _ _; simp
+
+theorem unused_intros': (n m: Nat) -> (m >= 0) :=
+  by
+    intros; simp
diff --git a/tests/lean/1204.lean.expected.out b/tests/lean/1204.lean.expected.out
new file mode 100644
index 0000000000..e69de29bb2