chore: cleanup

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)

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 }