From a014ae10018cff5c10fe448a9f5048ff923b326c Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 13 Mar 2025 13:24:24 +0100
Subject: [PATCH] fix: make `Term.mkAuxName` async-compatible (#7468)

---
 src/Lean/Elab/Term.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index d45e4ff610..027cdf1bd3 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1891,7 +1891,7 @@ def addAutoBoundImplicits' (xs : Array Expr) (type : Expr) (k : Array Expr → E
     forallBoundedTelescope (← mkForallFVars xs type) xs.size fun xs type => k xs type
 
 def mkAuxName (suffix : Name) : TermElabM Name := do
-  match (← read).declName? with
+  match (← read).declName? <|> (← getEnv).asyncPrefix? with
   | none          => Lean.mkAuxName (mkPrivateName (← getEnv) `aux) 1
   | some declName => Lean.mkAuxName (declName ++ suffix) 1