diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 5947e8fe35..12853453a3 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -825,14 +825,9 @@ fun stx _ => do
 @[builtinTermElab char] def elabChar : TermElab :=
 fun stx expectedType? => elabRawCharLit (stx.getArg 0) expectedType?
 
-def reflectName : Name → Expr
-| Name.anonymous => Lean.mkConst `Lean.Name.anonymous
-| Name.str n s _ => mkApp2 (Lean.mkConst `Lean.mkNameStr) (reflectName n) (mkStrLit s)
-| Name.num n i _ => mkApp2 (Lean.mkConst `Lean.mkNameNum) (reflectName n) (mkNatLit i)
-
 @[builtinTermElab quotedName] def elabQuotedName : TermElab :=
 fun stx _ => match_syntax stx with
-| `(`$n) => pure $ reflectName n.getId
+| `(`$n) => pure $ toExpr n.getId
 | _      => throwUnsupportedSyntax
 
 end Term