diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean
index 52e7d386b4..cd51896446 100644
--- a/src/Init/Lean/Elab/BuiltinNotation.lean
+++ b/src/Init/Lean/Elab/BuiltinNotation.lean
@@ -24,14 +24,14 @@ adaptExpander $ fun stx => match_syntax stx with
 
 @[builtinTermElab «if»] def elabIf : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `(if $h : $cond then $t else $e) => let h := mkTermIdFromIdent h; `(dite $cond (fun $h => $t) (fun $h => $e))
+| `(if $h : $cond then $t else $e) => `(dite $cond (fun $h:ident => $t) (fun $h:ident => $e))
 | `(if $cond then $t else $e)      => `(ite $cond $t $e)
 | _                                => throwUnsupportedSyntax
 
 @[builtinTermElab subtype] def elabSubtype : TermElab :=
 adaptExpander $ fun stx => match_syntax stx with
-| `({ $x : $type // $p }) => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : $type) => $p))
-| `({ $x // $p })         => let x := mkTermIdFromIdent x; `(Subtype (fun ($x : _) => $p))
+| `({ $x : $type // $p }) => `(Subtype (fun ($x:ident : $type) => $p))
+| `({ $x // $p })         => `(Subtype (fun ($x:ident : _) => $p))
 | _                       => throwUnsupportedSyntax
 
 @[builtinTermElab anonymousCtor] def elabAnoymousCtor : TermElab :=
@@ -66,8 +66,8 @@ adaptExpander $ fun stx => match_syntax stx with
 adaptExpander $ fun stx => match_syntax stx with
 | `(have $type from $val; $body)      => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $body) $val)
 | `(have $type := $val; $body)        => let thisId := mkTermIdFrom stx `this; `((fun ($thisId : $type) => $body) $val)
-| `(have $x : $type from $val; $body) => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
-| `(have $x : $type := $val; $body)   => let x := mkTermIdFromIdent x; `((fun ($x : $type) => $body) $val)
+| `(have $x : $type from $val; $body) => `((fun ($x:ident : $type) => $body) $val)
+| `(have $x : $type := $val; $body)   => `((fun ($x:ident : $type) => $body) $val)
 | _                                   => throwUnsupportedSyntax
 
 @[termElab «where»] def elabWhere : TermElab :=
diff --git a/src/Init/Lean/Elab/TermBinders.lean b/src/Init/Lean/Elab/TermBinders.lean
index a372590a2c..c689156353 100644
--- a/src/Init/Lean/Elab/TermBinders.lean
+++ b/src/Init/Lean/Elab/TermBinders.lean
@@ -187,10 +187,9 @@ private partial def expandFunBindersAux (binders : Array Syntax) : Syntax → Na
     let binder := binders.get ⟨i, h⟩;
     let processAsPattern : Unit → TermElabM (Array Syntax × Syntax) := fun _ => do {
       let pattern := binder;
-      ident ← mkFreshAnonymousIdent binder;
-      (binders, newBody) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder ident (mkHole binder));
-      let major := mkTermIdFromIdent ident;
-      newBody ← `(match $major with | $pattern => $newBody);
+      major ← mkFreshAnonymousIdent binder;
+      (binders, newBody) ← expandFunBindersAux body (i+1) (newBinders.push $ mkExplicitBinder major (mkHole binder));
+      newBody ← `(match $major:ident with | $pattern => $newBody);
       pure (binders, newBody)
     };
     match binder with