From 10fc908463cf1ae05fa3d0e1de5137d5ddb97edf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 6 Oct 2020 08:17:02 -0700
Subject: [PATCH] chore: use `Tactic.seq1` instead of
 `Tactic.tacticSeq1Indented`

Reason: antiquotations.
---
 src/Lean/Parser/Syntax.lean | 2 +-
 src/Lean/Parser/Term.lean   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Parser/Syntax.lean b/src/Lean/Parser/Syntax.lean
index 2834de6b9e..60c05f3d56 100644
--- a/src/Lean/Parser/Syntax.lean
+++ b/src/Lean/Parser/Syntax.lean
@@ -84,7 +84,7 @@ def optKindPrio : Parser := optional ("[" >> (parserKindPrio <|> parserKind <|>
 def macroArgSimple := parser! ident >> checkNoWsBefore "no space before ':'" >> ":" >> syntaxParser maxPrec
 def macroArg  := try strLit <|> try macroArgSimple
 def macroHead := macroArg <|> try ident
-def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.tacticSeq1Indented >> ")" <|> termParser)
+def macroTailTactic   : Parser := try (" : " >> identEq "tactic") >> darrow >> ("`(" >> toggleInsideQuot Tactic.seq1 >> ")" <|> termParser)
 def macroTailCommand  : Parser := try (" : " >> identEq "command") >> darrow >> ("`(" >> toggleInsideQuot (many1Unbox commandParser) >> ")" <|> termParser)
 def macroTailDefault  : Parser := try (" : " >> ident) >> darrow >> (("`(" >> toggleInsideQuot (categoryParserOfStack 2) >> ")") <|> termParser)
 def macroTail := macroTailTactic <|> macroTailCommand <|> macroTailDefault
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 2cad4d8135..ab49947c96 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -260,7 +260,7 @@ stx.isAntiquot || stx.isIdent
 end Term
 
 @[builtinTermParser 1] def Tactic.quot    : Parser := parser! "`(tactic|" >> toggleInsideQuot tacticParser >> ")"
-@[builtinTermParser]   def Tactic.quotSeq : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.tacticSeq1Indented >> ")"
+@[builtinTermParser]   def Tactic.quotSeq : Parser := parser! "`(tactic|" >> toggleInsideQuot Tactic.seq1 >> ")"
 
 @[builtinTermParser] def Level.quot  : Parser := parser! "`(level|" >> toggleInsideQuot levelParser >> ")"