diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 591535e769..b0fd848fc1 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -24,7 +24,7 @@ namespace Tactic
 def tacticSeq1Indented : Parser :=
 parser! many1Indent $ tacticParser >> optional "; "
 def tacticSeqBracketed : Parser :=
-parser! "{" >> sepBy tacticParser "; " true >> "}"
+parser! "{" >> many (tacticParser >> optional "; ") >> "}"
 def tacticSeq :=
 nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
 
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 9567027fb7..01f66d02c2 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -160,6 +160,15 @@ case b => exact y
 traceState
 repeat assumption
 
+theorem simple13b (x y z : Nat) : y = z → x = x → x = y → x = z := by {
+intros h1 h2 h3;
+traceState;
+apply @Eq.trans;
+case b => exact y;
+traceState;
+repeat assumption
+}
+
 theorem simple14 (x y z : Nat) : y = z → x = x → x = y → x = z := by
 intros
 apply @Eq.trans