chore: fix symm and label bugs from #3408

src/Init/Meta.lean

@@ -1429,24 +1429,6 @@ declare_simp_like_tactic (dsimp := true) dsimpAutoUnfold "dsimp! " fun (c : Lean
 
 end Tactic
 
-namespace Command
-
-/--
-Initialize a new "label" attribute.
-Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
--/
-macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
-  doc:(docComment)? "register_label_attr " id:ident : command => do
-  let str := id.getId.toString
-  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
-  let descr := quote (removeLeadingSpaces
-    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
-  `($[$doc:docComment]? initialize ext : LabelExtension ←
-      registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
-    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
-
-end Command
-
 end Parser
 
 end Lean

src/Init/Tactics.lean

@@ -1167,7 +1167,7 @@ syntax (name := normCastAddElim) "norm_cast_add_elim" ident : command
   It replaces the target with `u ~ t`.
 * `symm at h` will rewrite a hypothesis `h : t ~ u` to `h : u ~ t`.
 -/
-syntax (name := symm) "symm" (Parser.Tactic.location)? : tactic
+syntax (name := symm) "symm" (location)? : tactic
 
 /-- For every hypothesis `h : a ~ b` where a `@[symm]` lemma is available,
 add a hypothesis `h_symm : b ~ a`. -/

src/Lean/Elab/Tactic/Symm.lean

@@ -12,10 +12,11 @@ namespace Lean.Elab.Tactic
 @[builtin_tactic Lean.Parser.Tactic.symm]
 def evalSymm : Tactic := fun stx =>
   match stx with
-  | `(tactic| symm $(loc)) => do
+  | `(tactic| symm $(loc?)?) => do
     let atHyp h := liftMetaTactic1 fun g => g.applySymmAt h
     let atTarget := liftMetaTactic1 fun g => g.applySymm
-    withLocation (expandOptLocation loc) atHyp atTarget fun _ => throwError "symm made no progress"
+    let loc := if let some loc := loc? then expandLocation loc else Location.targets #[] true
+    withLocation loc atHyp atTarget fun _ => throwError "symm made no progress"
   | _ => throwUnsupportedSyntax
 
 @[builtin_tactic Lean.Parser.Tactic.symmSaturate]

src/Lean/LabelAttribute.lean

@@ -72,6 +72,20 @@ def registerLabelAttr (attrName : Name) (attrDescr : String)
   labelExtensionMapRef.modify fun map => map.insert attrName ext
   return ext
 
+/--
+Initialize a new "label" attribute.
+Declarations tagged with the attribute can be retrieved using `Std.Tactic.LabelAttr.labelled`.
+-/
+macro (name := _root_.Lean.Parser.Command.registerLabelAttr)
+  doc:(docComment)? "register_label_attr " id:ident : command => do
+  let str := id.getId.toString
+  let idParser := mkIdentFrom id (`Parser.Attr ++ id.getId)
+  let descr := quote (removeLeadingSpaces
+    (doc.map (·.getDocString) |>.getD ("labelled declarations for " ++ id.getId.toString)))
+  `($[$doc:docComment]? initialize ext : Lean.LabelExtension ←
+      registerLabelAttr $(quote id.getId) $descr $(quote id.getId)
+    $[$doc:docComment]? syntax (name := $idParser:ident) $(quote str):str : attr)
+
 /-- When `attrName` is an attribute created using `register_labelled_attr`,
 return the names of all declarations labelled using that attribute. -/
 def labelled (attrName : Name) : CoreM (Array Name) := do