From 312ea061b1618c5bfc2854badd3052e44c14985c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Jan 2020 11:43:03 -0800
Subject: [PATCH] chore: use `toExpr`

cc @Kha
---
 src/Init/Lean/Elab/Term.lean | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

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