diff --git a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
index 66bf723010..35489c159a 100644
--- a/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
+++ b/src/Lean/Elab/Tactic/Do/VCGen/Basic.lean
@@ -88,19 +88,11 @@ def ifOutOfFuel (x : VCGenM α) (k : VCGenM α) : VCGenM α := do
   | Fuel.limited 0 => x
   | _ => k
 
-def withFreshUserNames (k : VCGenM α) : VCGenM α := do
-  let mut lctx ← getLCtx
-  for i in [(← read).initialCtxSize:lctx.numIndices] do
-    let some decl := lctx.decls[i]! | continue
-    let n := decl.userName
-    if !n.hasMacroScopes then
-      lctx := lctx.setUserName decl.fvarId (← mkFreshUserName n)
-  withLCtx' lctx k
-
-def emitVC (subGoal : Expr) (name : Name) : VCGenM Expr := withFreshUserNames do
-  let m ← liftM <| mkFreshExprSyntheticOpaqueMVar subGoal (tag := name)
-  modify fun s => { s with vcs := s.vcs.push m.mvarId! }
-  return m
+def emitVC (subGoal : Expr) (name : Name) : VCGenM Expr := do
+  withFreshUserNamesSinceIdx (← read).initialCtxSize do
+    let m ← liftM <| mkFreshExprSyntheticOpaqueMVar subGoal (tag := name)
+    modify fun s => { s with vcs := s.vcs.push m.mvarId! }
+    return m
 
 def addSubGoalAsVC (goal : MVarId) : VCGenM PUnit := do
   modify fun s => { s with vcs := s.vcs.push goal }
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 627d9dcdd0..f867a85214 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -1951,6 +1951,18 @@ def withErasedFVars [MonadLCtx n] [MonadLiftT MetaM n] (fvarIds : Array FVarId)
   let localInsts' := localInsts.filter (!fvarIds.contains ·.fvar.fvarId!)
   withLCtx lctx' localInsts' k
 
+/--
+Ensures that the user names of all local declarations after index `idx` have a macro scope.
+-/
+def withFreshUserNamesSinceIdx [MonadLCtx n] [MonadLiftT MetaM n] (idx : Nat) (k : n α) : n α := do
+  let mut lctx ← getLCtx
+  for i in [idx:lctx.numIndices] do
+    let some decl := lctx.decls[i]! | continue
+    let n := decl.userName
+    if !n.hasMacroScopes then
+      lctx := lctx.setUserName decl.fvarId (← liftMetaM <| mkFreshUserName n)
+  withLCtx' lctx k
+
 private def withMVarContextImp (mvarId : MVarId) (x : MetaM α) : MetaM α := do
   let mvarDecl ← mvarId.getDecl
   withLocalContextImp mvarDecl.lctx mvarDecl.localInstances x