diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 851cc3e171d7..a0f6310d1263 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -92,7 +92,7 @@ Returns the declaration name.
 -/
 def declareTacticSyntax (tactic : Syntax) (name? : Option Name := none) : TermElabM Name :=
   withFreshMacroScope do
-    let name ← name?.getDM do MonadQuotation.addMacroScope ((← getEnv).asyncPrefix?.getD .anonymous ++ `_auto)
+    let name ← name?.getDM (mkAuxDeclName `_auto)
     let type := Lean.mkConst `Lean.Syntax
     let value ← quoteAutoTactic tactic
     trace[Elab.autoParam] value
diff --git a/tests/lean/run/3257.lean b/tests/lean/run/3257.lean
index 942672164143..a066b5136a2d 100644
--- a/tests/lean/run/3257.lean
+++ b/tests/lean/run/3257.lean
@@ -15,7 +15,7 @@ example : U := by
 
 /--
 trace: [Meta.Tactic.simp.discharge] bar discharge ✅️
-      autoParam T _auto✝
+      autoParam T bar._auto_1
   [Meta.Tactic.simp.rewrite] T.mk:1000:
         T
       ==>
diff --git a/tests/lean/run/cleanup_forallTelescope.lean b/tests/lean/run/cleanup_forallTelescope.lean
index b2f90d5883ae..4a38c07a1881 100644
--- a/tests/lean/run/cleanup_forallTelescope.lean
+++ b/tests/lean/run/cleanup_forallTelescope.lean
@@ -29,7 +29,7 @@ def f (x := 0) (_ : x = x := by rfl) : Nat := x+1
 
 
 /--
-info: (x : optParam Nat 0) → autoParam (x = x) _auto✝ → Nat
+info: (x : optParam Nat 0) → autoParam (x = x) f._auto_1 → Nat
 ---
 (x : Nat) → x = x → Nat
 -/