diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
index 74a6b35c2e..a94b2e5eca 100644
--- a/src/Init/Lean/Parser/Tactic.lean
+++ b/src/Init/Lean/Parser/Tactic.lean
@@ -37,7 +37,7 @@ def ident' : Parser := ident <|> underscore
 /-
   We must not use the `parser! t` macro here it because it expands into `mkAntiquot ... <|> t`,
   but a tactic parser may start with an antiquotation. -/
-def seq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
+def seq : Parser         := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
 def nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
 
 @[builtinTacticParser] def «intro»      := parser! nonReservedSymbol "intro " >> optional ident'