From 10102bf3706be28197d76016c2f3de8ec2ecf5b9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Dec 2020 07:47:28 -0800
Subject: [PATCH] chore: remove "local" before `attribute` command

`local` is now part of the `Term.attrInstance` parser.
---
 src/Lean/Elab/Declaration.lean | 7 +++----
 src/Lean/Parser/Command.lean   | 2 +-
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 53a5d60c87..e6519ee02c 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -250,11 +250,10 @@ def elabMutual : CommandElab := fun stx => do
   else
     throwError "invalid mutual block"
 
-/- parser! optional "local " >> "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "]" >> many1 ident -/
+/- parser! "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "]" >> many1 ident -/
 @[builtinCommandElab «attribute»] def elabAttr : CommandElab := fun stx => do
-  -- let persistent := stx[0].isNone -- TODO: remove
-  let attrs ← elabAttrs stx[3]
-  let idents := stx[5].getArgs
+  let attrs ← elabAttrs stx[2]
+  let idents := stx[4].getArgs
   for ident in idents do withRef ident $ liftTermElabM none do
     let declName ← resolveGlobalConstNoOverload ident.getId
     Term.applyAttributes declName attrs
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 0365c53696..d9f7bea495 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -81,7 +81,7 @@ declModifiers false >> («abbrev» <|> «def» <|> «theorem» <|> «constant»
 @[builtinCommandParser] def «resolve_name» := parser! "#resolve_name " >> ident
 @[builtinCommandParser] def «init_quot»    := parser! "init_quot"
 @[builtinCommandParser] def «set_option»   := parser! "set_option " >> ident >> (nonReservedSymbol "true" <|> nonReservedSymbol "false" <|> strLit <|> numLit)
-@[builtinCommandParser] def «attribute»    := parser! optional "local " >> "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "] " >> many1 ident
+@[builtinCommandParser] def «attribute»    := parser! "attribute " >> "[" >> sepBy1 Term.attrInstance ", " >> "] " >> many1 ident
 @[builtinCommandParser] def «export»       := parser! "export " >> ident >> "(" >> many1 ident >> ")"
 def openHiding       := parser! atomic (ident >> "hiding") >> many1 ident
 def openRenamingItem := parser! ident >> unicodeSymbol "→" "->" >> ident