From 22dc784c3e588ff3016d43820edae74fd42e1461 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 18 Sep 2020 11:37:51 -0700
Subject: [PATCH] chore: cleanup

---
 src/Lean/Elab/Term.lean | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 3cd6d585b3..cba01f4b0b 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -426,9 +426,7 @@ pure e
   Auxiliary method for creating fresh binder names.
   Do not confuse with the method for creating fresh free/meta variable ids. -/
 def mkFreshUserName : TermElabM Name :=
-withFreshMacroScope do
-  x ← `(x);
-  pure x.getId
+withFreshMacroScope $ MonadQuotation.addMacroScope `x
 
 /--
   Auxiliary method for creating a `Syntax.ident` containing
@@ -441,9 +439,7 @@ pure $ mkIdentFrom ref n
 /--
   Auxiliary method for creating binder names for local instances. -/
 def mkFreshInstanceName : TermElabM Name :=
-withFreshMacroScope do
-  inst ← `(inst);
-  pure inst.getId
+withFreshMacroScope $ MonadQuotation.addMacroScope `inst
 
 private partial def hasCDot : Syntax → Bool
 | Syntax.node k args =>