diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 13f38a31f6..23b05d2a04 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -394,7 +394,7 @@ macro "let' " d:letDecl : tactic => `(refine_lift' let $d:letDecl; ?_)
 
 syntax inductionAlt  := ppDedent(ppLine) "| " (group("@"? ident) <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
 syntax inductionAlts := "with " (tactic)? withPosition( (colGe inductionAlt)+)
-syntax (name := induction) "induction " term,+ (" using " ident)?  ("generalizing " term:max+)? (inductionAlts)? : tactic
+syntax (name := induction) "induction " term,+ (" using " ident)?  ("generalizing " (colGt term:max)+)? (inductionAlts)? : tactic
 
 syntax generalizeArg := atomic(ident " : ")? term:51 " = " ident
 /--
diff --git a/tests/lean/run/inductionParse.lean b/tests/lean/run/inductionParse.lean
new file mode 100644
index 0000000000..5421f3ebda
--- /dev/null
+++ b/tests/lean/run/inductionParse.lean
@@ -0,0 +1,4 @@
+example (a b : Nat) : True := by
+  induction a generalizing b
+  case zero => trivial
+  case succ => trivial