diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 484e941a68..96a49ad6bf 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -28,10 +28,11 @@ private def expandBinderIdent (stx : Syntax) : TermElabM Syntax :=
 
 /-- Given syntax of the form `(ident >> " : ")?`, return `ident`, or a new instance name. -/
 private def expandOptIdent (stx : Syntax) : TermElabM Syntax := do
-  if stx.getNumArgs == 0 then
-    pure $ mkIdentFrom stx (← mkFreshInstanceName)
+  if stx.isNone then
+    let id ← withFreshMacroScope <| MonadQuotation.addMacroScope `inst
+    return mkIdentFrom stx id
   else
-    pure stx[0]
+    return stx[0]
 
 structure BinderView :=
   (id : Syntax)
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 24061bbb1b..625fe5cca4 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -465,11 +465,6 @@ def mkFreshBinderName : TermElabM Name :=
 def mkFreshIdent (ref : Syntax) : TermElabM Syntax :=
   return mkIdentFrom ref (← mkFreshBinderName)
 
-/--
-  Auxiliary method for creating binder names for local instances. -/
-def mkFreshInstanceName : TermElabM Name :=
-  withFreshMacroScope $ MonadQuotation.addMacroScope `inst
-
 private def liftAttrM {α} (x : AttrM α) : TermElabM α := do
   let ctx ← read
   liftCoreM $ x.run { currNamespace := ctx.currNamespace, openDecls := ctx.openDecls }