diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean
index b20d43f388..35071ddf51 100644
--- a/src/Lean/Elab/ElabRules.lean
+++ b/src/Lean/Elab/ElabRules.lean
@@ -95,8 +95,7 @@ def elabElab : CommandElab
     -- name
     let name ← match name? with
       | some name => pure name.getId
-      | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-    let name ← addMacroScopeIfLocal name attrKind
+      | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)) attrKind
     let nameId := name?.getD (mkIdentFrom tk name (canonical := true))
     let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
     elabCommand <|← `(
diff --git a/src/Lean/Elab/Macro.lean b/src/Lean/Elab/Macro.lean
index ed0e3df779..93059a6c35 100644
--- a/src/Lean/Elab/Macro.lean
+++ b/src/Lean/Elab/Macro.lean
@@ -20,8 +20,7 @@ open Lean.Parser.Command
       -- name
       let name ← match name? with
         | some name => pure name.getId
-        | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
-      let name ← addMacroScopeIfLocal name attrKind
+        | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)) attrKind
       /- The command `syntax [<kind>] ...` adds the current namespace to the syntax node kind.
         So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/
       let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩
diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index 4fb93b3eac..f7b9a284fd 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -126,8 +126,7 @@ private def expandNotationAux (ref : Syntax) (currNamespace : Name)
   let name ←
     match name? with
     | some name => pure name.getId
-    | none => mkNameFromParserSyntax `term (mkNullNode syntaxParts)
-  let name ← addMacroScopeIfLocal name attrKind
+    | none => addMacroScopeIfLocal (← mkNameFromParserSyntax `term (mkNullNode syntaxParts)) attrKind
   -- build macro rules
   let vars := items.filter fun item => item.raw.getKind == ``identPrec
   let vars := vars.map fun var => var.raw[0]
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 04b50eedf7..165c8e4663 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -375,8 +375,7 @@ def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind :
     | none      => pure precDefault
   let name ← match name? with
     | some name => pure name.getId
-    | none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser
-  let name ← addMacroScopeIfLocal name attrKind
+    | none => addMacroScopeIfLocal (← liftMacroM <| mkNameFromParserSyntax cat syntaxParser) attrKind
   trace[Meta.debug] "name: {name}"
   let prio ← liftMacroM <| evalOptPrio prio?
   let idRef := (name?.map (·.raw)).getD tk
diff --git a/tests/lean/run/2009.lean b/tests/lean/run/2009.lean
new file mode 100644
index 0000000000..f945effd82
--- /dev/null
+++ b/tests/lean/run/2009.lean
@@ -0,0 +1 @@
+local notation (name := foo) "foo" => 42