From 2733a5bebd3df6ad426cea908a56c93a095317dc Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 28 Nov 2019 05:40:03 -0800
Subject: [PATCH] chore: remove unnecessary method

---
 src/Init/Lean/Meta/Basic.lean | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index b5f1ae37f3..72d91b5696 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -204,14 +204,11 @@ do s ← get;
    modify $ fun s => { ngen := s.ngen.next, .. s };
    pure id
 
-def mkFreshExprMVarAt (lctx : LocalContext) (type : Expr) (userName : Name := Name.anonymous) (synthetic : Bool := false) : MetaM Expr :=
-do mvarId ← mkFreshId;
-   modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId userName lctx type synthetic, .. s };
-   pure $ mkMVar mvarId
-
 def mkFreshExprMVar (type : Expr) (userName : Name := Name.anonymous) (synthetic : Bool := false) : MetaM Expr :=
 do lctx ← getLCtx;
-   mkFreshExprMVarAt lctx type userName synthetic
+   mvarId ← mkFreshId;
+   modify $ fun s => { mctx := s.mctx.addExprMVarDecl mvarId userName lctx type synthetic, .. s };
+   pure $ mkMVar mvarId
 
 def mkFreshLevelMVar : MetaM Level :=
 do mvarId ← mkFreshId;