From 85d8c4fa855b6356dac990ba50ee84918210272f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 15:42:36 -0700
Subject: [PATCH] chore: add proper kind for `tacticSeq1Indented`

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

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 3954dabf42..f693c408ec 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -22,12 +22,12 @@ categoryParser `tactic rbp
 namespace Tactic
 
 def tacticSeq1Indented : Parser :=
-node `Lean.Parser.Tactic.seq $ withPosition $
+parser! withPosition $
   sepBy1 tacticParser (try ("; " >>  checkColGe "tatic must be indented"))
 def tacticSeqBracketed : Parser :=
-  parser! "{" >> sepBy tacticParser "; " true >> "}"
+parser! "{" >> sepBy tacticParser "; " true >> "}"
 def tacticSeq :=
-  nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
+nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
 
 /- Raw sequence for quotation and grouping -/
 def seq1 :=