From aa410283c6ac18d339e5ccfe7bb3ab30f31e807a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 15:38:41 -0700
Subject: [PATCH] fix: we don't want antiquotation for `seq1`

---
 src/Lean/Parser/Term.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 7baa65f125..3954dabf42 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -30,7 +30,8 @@ def tacticSeq :=
   nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
 
 /- Raw sequence for quotation and grouping -/
-def seq1 := parser! sepBy1 tacticParser "; " true
+def seq1 :=
+node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser "; " true
 
 end Tactic