diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 577df0bb8f..979b69219a 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -199,13 +199,13 @@ syntax[«let!»] "let! " letDecl : tactic
 syntax[letrec] withPosition(atomic(group("let " &"rec ")) letRecDecls) : tactic
 
 syntax inductionAlt  := (ident <|> "_") (ident <|> "_")* " => " (hole <|> syntheticHole <|> tacticSeq)
-syntax inductionAlts := "with " withPosition("| " sepBy1(inductionAlt, colGe "| "))
+syntax inductionAlts := "with " withPosition("| " sepBy1(inductionAlt, "| ", colGe "| "))
 syntax[induction] "induction " sepBy1(term, ", ") (" using " ident)?  ("generalizing " ident+)? (inductionAlts)? : tactic
 syntax casesTarget := atomic(ident " : ")? term
 syntax[cases] "cases " sepBy1(casesTarget, ", ") (" using " ident)? (inductionAlts)? : tactic
 
 syntax matchAlt  := sepBy1(term, ", ") " => " (hole <|> syntheticHole <|> tacticSeq)
-syntax matchAlts := withPosition("| " sepBy1(matchAlt, colGe "| "))
+syntax matchAlts := withPosition("| " sepBy1(matchAlt, "| ", colGe "| "))
 syntax[«match»] "match " sepBy1(matchDiscr, ", ") (" : " term)? " with " matchAlts : tactic
 
 syntax[introMatch] "intro " matchAlts : tactic