diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 440672bd32..8640925132 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -483,11 +483,6 @@ fun n => do
   else
     elabOpenRenaming body
 
-/- We just ignore Lean3 notation declaration commands. -/
-@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
-@[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()
-@[builtinCommandElab «notation»] def elabNotation : CommandElab := fun _ => pure ()
-
 @[builtinCommandElab «variable»] def elabVariable : CommandElab :=
 fun n => do
   -- `variable` bracktedBinder
diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean
index 66c9ad1751..b1766567f9 100644
--- a/src/Init/Lean/Elab/Syntax.lean
+++ b/src/Init/Lean/Elab/Syntax.lean
@@ -173,6 +173,11 @@ adaptExpander $ fun stx => match_syntax stx with
   `(@[macro $(Lean.mkSimpleIdent k)] def myMacro : Macro := fun stx => match_syntax stx with $alts* | _ => throw ())
 | _ => throwUnsupportedSyntax
 
+/- We just ignore Lean3 notation declaration commands. -/
+@[builtinCommandElab «mixfix»] def elabMixfix : CommandElab := fun _ => pure ()
+@[builtinCommandElab «reserve»] def elabReserve : CommandElab := fun _ => pure ()
+@[builtinCommandElab «notation»] def elabNotation : CommandElab := fun _ => pure ()
+
 end Command
 end Elab
 end Lean