diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean index d773625acc..18c77e696a 100644 --- a/src/Init/Lean/Elab/Syntax.lean +++ b/src/Init/Lean/Elab/Syntax.lean @@ -168,7 +168,7 @@ fun stx => do trace `Elab stx $ fun _ => d; withMacroExpansion stx $ elabCommand d -@[builtinCommandElab «macro_rules»] def elabMacro : CommandElab := +@[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab := adaptExpander $ fun stx => match_syntax stx with | `(macro_rules $alts*) => do -- TODO: clean up with matchAlt quotation