diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean
index 14b2d68e14..ef7671ce27 100644
--- a/src/Init/Tactics.lean
+++ b/src/Init/Tactics.lean
@@ -788,7 +788,7 @@ syntax inductionAlt  := ppDedent(ppLine) inductionAltLHS+ " => " (hole <|> synth
 After `with`, there is an optional tactic that runs on all branches, and
 then a list of alternatives.
 -/
-syntax inductionAlts := " with" (ppSpace tactic)? withPosition((colGe inductionAlt)+)
+syntax inductionAlts := " with" (ppSpace colGt tactic)? withPosition((colGe inductionAlt)+)
 
 /--
 Assuming `x` is a variable in the local context with an inductive type,
diff --git a/tests/lean/inductionParse.lean b/tests/lean/inductionParse.lean
new file mode 100644
index 0000000000..b9779b8e2b
--- /dev/null
+++ b/tests/lean/inductionParse.lean
@@ -0,0 +1,5 @@
+/-! should not parse `done` as part of `induction` -/
+
+example (a : Nat) : True := by
+  induction a with
+  done
diff --git a/tests/lean/inductionParse.lean.expected.out b/tests/lean/inductionParse.lean.expected.out
new file mode 100644
index 0000000000..da90e48b91
--- /dev/null
+++ b/tests/lean/inductionParse.lean.expected.out
@@ -0,0 +1 @@
+inductionParse.lean:4:18-5:6: error: unexpected identifier; expected '|'
diff --git a/tests/lean/run/inductionParse.lean b/tests/lean/run/inductionParse.lean
index 5421f3ebda..612bc07e73 100644
--- a/tests/lean/run/inductionParse.lean
+++ b/tests/lean/run/inductionParse.lean
@@ -1,3 +1,5 @@
+/-! should not parse `case` as a `generalizing` variable -/
+
 example (a b : Nat) : True := by
   induction a generalizing b
   case zero => trivial