diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 41923ad3a0..aed9978afe 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -9,6 +9,7 @@ import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.SetOption
 import Lean.Language.Basic
+import Lean.Meta.ForEachExpr
 
 namespace Lean.Elab.Command
 
@@ -719,9 +720,16 @@ def runTermElabM (elabFn : Array Expr → TermElabM α) : CommandElabM α := do
           -- We don't want to store messages produced when elaborating `(getVarDecls s)` because they have already been saved when we elaborated the `variable`(s) command.
           -- So, we use `Core.resetMessageLog`.
           Core.resetMessageLog
-          let someType := mkSort levelZero
-          Term.addAutoBoundImplicits' xs someType fun xs _ =>
+          let xs ← Term.addAutoBoundImplicits xs none
+          if xs.all (·.isFVar) then
             Term.withoutAutoBoundImplicit <| elabFn xs
+          else
+            -- Abstract any mvars that appear in `xs` using `mkForallFVars` (the type `mkSort levelZero` is an arbitrary placeholder)
+            -- and then rebuild the local context from scratch.
+            -- Resetting prevents the local context from including the original fvars from `xs`.
+            let ctxType ← Meta.mkForallFVars' xs (mkSort levelZero)
+            Meta.withLCtx {} {} <| Meta.forallBoundedTelescope ctxType xs.size fun xs _ =>
+              Term.withoutAutoBoundImplicit <| elabFn xs
 
 private def liftAttrM {α} (x : AttrM α) : CommandElabM α := do
   liftCoreM x
diff --git a/tests/lean/run/autoboundIssues.lean b/tests/lean/run/autoboundIssues.lean
index 95d1233f96..afcd15a3cc 100644
--- a/tests/lean/run/autoboundIssues.lean
+++ b/tests/lean/run/autoboundIssues.lean
@@ -1,10 +1,92 @@
+/-!
+# Regression tests for auto-bound implicits
+-/
+
+set_option pp.mvars false
+
+/-!
+Auto-bound implicit appears in dot notation in the type, for a variable that appears later.
+-/
 example : n.succ = 1 → n = 0 := by
   intros h; injection h
 
+/-!
+Auto-bound implicit appears in dot notation in a binder, for a variable that appears later.
+-/
 example (h : n.succ = 1) : n = 0 := by
   injection h
 
+/-!
+Auto-bound implicit appears as argument to notation that is postponed.
+The type of `σ` is specialized to `T` later.
+-/
 opaque T : Type
 opaque T.Pred : T → T → Prop
 
 example {ρ} (hρ : ρ.Pred σ) : T.Pred ρ ρ := sorry
+
+
+namespace TestRunTermElab
+/-!
+In the following tests, there is an auto-bound implicit whose type is a metavariable,
+which gets turned into an additional variable.
+-/
+
+def constUnit (a : A) : Type := Unit
+
+/-!
+The auto-bound implicit creates a new variable `A✝`, which comes from the argument name in `constUnit`.
+(This has been the case well before the creation of this test.)
+-/
+/--
+info: A✝ : Sort u_1
+a : A✝
+_x : constUnit a
+⊢ True
+-/
+#guard_msgs in
+example (_x : constUnit a) : True := by
+  trace_state
+  trivial
+
+variable (x : constUnit a)
+
+/-!
+The local context here used to be
+```
+a✝ : ?_
+x✝¹ : constUnit a✝
+x✝ : Sort ?_
+a : x✝
+x : constUnit a
+⊢ True
+```
+Note the duplication and `x✝` for the name of the metavariable-as-a-variable.
+The duplication was because `runTermElabM` wasn't resetting the local context.
+The poor variable name was due to using `mkForallFVars` instead of `mkForallFVars'`.
+-/
+/--
+info: A✝ : Sort _
+a : A✝
+x : constUnit a
+⊢ True
+-/
+#guard_msgs in
+example : True := by
+  trace_state
+  trivial
+
+/-!
+Checking that `#check` also has the improvement.
+-/
+/--
+info: 1 : Nat
+---
+info: A✝ : Sort _
+a : A✝
+x : constUnit a
+⊢ ?_
+-/
+#guard_msgs in #check (by trace_state; exact 1)
+
+end TestRunTermElab