From d4c1432574cc10bc9294b6a3fff887bda5dfe27b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 16:24:27 -0700
Subject: [PATCH] fix: `tacticSeqBracketed`

---
 src/Lean/Parser/Term.lean        | 2 +-
 tests/lean/run/newfrontend1.lean | 9 +++++++++
 2 files changed, 10 insertions(+), 1 deletion(-)

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