diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean
index a47bab0bfc..b20d43f388 100644
--- a/src/Lean/Elab/ElabRules.lean
+++ b/src/Lean/Elab/ElabRules.lean
@@ -96,6 +96,7 @@ def elabElab : CommandElab
     let name ← match name? with
       | some name => pure name.getId
       | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
+    let name ← addMacroScopeIfLocal name 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 890db271f6..ed0e3df779 100644
--- a/src/Lean/Elab/Macro.lean
+++ b/src/Lean/Elab/Macro.lean
@@ -21,6 +21,7 @@ open Lean.Parser.Command
       let name ← match name? with
         | some name => pure name.getId
         | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts)
+      let name ← addMacroScopeIfLocal name 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 710f6d728c..4fb93b3eac 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -113,11 +113,6 @@ def mkSimpleDelab (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT Ma
       | `($lhs $$moreArgs*) => withRef f `($pat $$moreArgs*)
       | _                   => throw ())
 
-private def isLocalAttrKind (attrKind : Syntax) : Bool :=
-  match attrKind with
-  | `(Parser.Term.attrKind| local) => true
-  | _ => false
-
 private def expandNotationAux (ref : Syntax) (currNamespace : Name)
     (doc? : Option (TSyntax ``docComment))
     (attrs? : Option (TSepArray ``attrInstance ","))
@@ -132,6 +127,7 @@ private def expandNotationAux (ref : Syntax) (currNamespace : Name)
     match name? with
     | some name => pure name.getId
     | none => mkNameFromParserSyntax `term (mkNullNode syntaxParts)
+  let name ← addMacroScopeIfLocal name 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 641f739e4a..04b50eedf7 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -345,6 +345,20 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
   <|>
   throwError "invalid syntax node kind '{k}'"
 
+def isLocalAttrKind (attrKind : Syntax) : Bool :=
+  match attrKind with
+  | `(Parser.Term.attrKind| local) => true
+  | _ => false
+
+/--
+Add macro scope to `name` if it does not already have them, and `attrKind` is `local`.
+-/
+def addMacroScopeIfLocal [MonadQuotation m] [Monad m] (name : Name) (attrKind : Syntax) : m Name := do
+  if isLocalAttrKind attrKind && !name.hasMacroScopes then
+    MonadQuotation.addMacroScope name
+  else
+    return name
+
 @[builtin_command_elab «syntax»] def elabSyntax : CommandElab := fun stx => do
   let `($[$doc?:docComment]? $[ @[ $attrInstances:attrInstance,* ] ]? $attrKind:attrKind
       syntax%$tk $[: $prec? ]? $[(name := $name?)]? $[(priority := $prio?)]? $[$ps:stx]* : $catStx) := stx
@@ -362,6 +376,8 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do
   let name ← match name? with
     | some name => pure name.getId
     | none => liftMacroM <| mkNameFromParserSyntax cat syntaxParser
+  let name ← addMacroScopeIfLocal name attrKind
+  trace[Meta.debug] "name: {name}"
   let prio ← liftMacroM <| evalOptPrio prio?
   let idRef := (name?.map (·.raw)).getD tk
   let stxNodeKind := (← getCurrNamespace) ++ name
diff --git a/tests/pkg/misc/Misc.lean b/tests/pkg/misc/Misc.lean
index ec165e72ce..fc3063b40f 100644
--- a/tests/pkg/misc/Misc.lean
+++ b/tests/pkg/misc/Misc.lean
@@ -1,4 +1,5 @@
 import Misc.Foo
+import Misc.Boo
 import Lean
 
 open Lean Meta
diff --git a/tests/pkg/misc/Misc/Boo.lean b/tests/pkg/misc/Misc/Boo.lean
new file mode 100644
index 0000000000..406fb8e0c2
--- /dev/null
+++ b/tests/pkg/misc/Misc/Boo.lean
@@ -0,0 +1,3 @@
+local infix:50 " ≺ " => LE.le
+
+#check 1 ≺ 2
diff --git a/tests/pkg/misc/Misc/Foo.lean b/tests/pkg/misc/Misc/Foo.lean
index 077786d034..3389620db5 100644
--- a/tests/pkg/misc/Misc/Foo.lean
+++ b/tests/pkg/misc/Misc/Foo.lean
@@ -7,3 +7,7 @@ open Lean Meta
   return ()
 
 def foo := 42
+
+local infix:50 " ≺ " => LE.le
+
+#check 1 ≺ 2