diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean
index 6291658b34..ab72486838 100644
--- a/src/Lean/Elab/Notation.lean
+++ b/src/Lean/Elab/Notation.lean
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Syntax
+import Lean.Elab.AuxDef
 
 namespace Lean.Elab.Command
 open Lean.Syntax
@@ -52,12 +53,14 @@ def mkSimpleDelab (attrKind : Syntax) (vars : Array Syntax) (pat qrhs : Syntax)
     guard <| args.all (Syntax.isIdent ∘ getAntiquotTerm)
     guard <| args.allDiff
     -- replace head constant with (unused) antiquotation so we're not dependent on the exact pretty printing of the head
-    `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander := fun
+    `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident]
+      aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
        | `($$(_):ident $args*) => `($pat)
        | _                     => throw ())
   | `($c:ident)        =>
     let [(c, [])] ← Macro.resolveGlobalName c.getId | failure
-    `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident] def unexpand : Lean.PrettyPrinter.Unexpander
+    `(@[$attrKind:attrKind appUnexpander $(mkIdent c):ident]
+      aux_def unexpand $(mkIdent c) : Lean.PrettyPrinter.Unexpander := fun
        | `($$(_):ident) => `($pat)
        | _              => throw ())
   | _                  => failure
diff --git a/tests/lean/ppNotationCode.lean.expected.out b/tests/lean/ppNotationCode.lean.expected.out
index ef2c66bafc..1a31b2e879 100644
--- a/tests/lean/ppNotationCode.lean.expected.out
+++ b/tests/lean/ppNotationCode.lean.expected.out
@@ -1,7 +1,7 @@
 [Elab.definition.body] «term_+++_» : Lean.TrailingParserDescr :=
 Lean.ParserDescr.trailingNode `«term_+++_» 45 46
   (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "+++") (Lean.ParserDescr.cat `term 46))
-[Elab.definition.body] _aux.ppNotationCode._.macroRules.«term_+++__1» : Lean.Macro :=
+[Elab.definition.body] _aux_ppNotationCode___macroRules_«term_+++_»_1 : Lean.Macro :=
 fun x =>
   let discr := x;
   if Lean.Syntax.isOfKind discr `«term_+++_» = true then
@@ -22,7 +22,7 @@ fun x =>
   else
     let discr := x;
     throw Lean.Macro.Exception.unsupportedSyntax
-[Elab.definition.body] unexpand._@.ppNotationCode._hyg.6 : Lean.PrettyPrinter.Unexpander :=
+[Elab.definition.body] _aux_ppNotationCode___unexpand_Nat_add_1 : Lean.PrettyPrinter.Unexpander :=
 fun x =>
   let discr := x;
   if Lean.Syntax.isOfKind discr `Lean.Parser.Term.app = true then