From c49ccda46ac3e968edd5f8e1633d54e26ba20072 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Sep 2020 14:51:20 -0700
Subject: [PATCH] feat: add antiquotation for `indentedNonEmptySeq`

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

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 591afb4ecd..aa0e139796 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -20,7 +20,7 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
 categoryParser `tactic rbp
 
 def Tactic.indentedNonEmptySeq : Parser :=
-node `Lean.Parser.Tactic.seq $ withPosition fun pos =>
+nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.seq $ withPosition fun pos =>
   sepBy1 tacticParser (try ("; " >>  checkColGe pos.column "tatic must be indented"))
 
 def darrow : Parser := " => "