diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index c121e3ecc7..87fb681eaf 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -95,6 +95,26 @@ stx.ifNode
     | none      => logError stx ("command '" ++ toString k ++ "' has not been implemented"))
   (fun _ => logErrorUsingCmdPos ("unexpected command"))
 
+@[specialize] def runTermElabM {α} (x : TermElabM α) : CommandElabM α :=
+fun ctx s =>
+  let scope := s.scopes.head!;
+  let termCtx : Term.Context := {
+    config         := { opts := scope.options, foApprox := true, ctxApprox := true, quasiPatternApprox := true, isDefEqStuckEx := true },
+    fileName       := ctx.fileName,
+    fileMap        := ctx.fileMap,
+    cmdPos         := s.cmdPos,
+    ns             := scope.ns,
+    univNames      := scope.univNames,
+    openDecls      := scope.openDecls
+  };
+  let termState : Term.State := {
+    env      := s.env,
+    messages := s.messages
+  };
+  match x termCtx termState with
+  | EStateM.Result.ok a newS     => EStateM.Result.ok a { env := newS.env, messages := newS.messages, .. s }
+  | EStateM.Result.error ex newS => EStateM.Result.error ex { env := newS.env, messages := newS.messages, .. s }
+
 def getEnv : CommandElabM Environment :=
 do s ← get; pure s.env
 
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index fea9acce85..4d5f5fd90c 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -18,6 +18,7 @@ structure Context extends Meta.Context :=
 (fileMap     : FileMap)
 (cmdPos      : String.Pos)
 (ns          : Name) -- current Namespace
+(univNames   : List Name := [])
 (openDecls   : List OpenDecl := [])
 
 inductive SyntheticMVarInfo
@@ -80,7 +81,7 @@ abbrev TermElabAttribute := ElabAttribute TermElabTable
 def mkTermElabAttribute : IO TermElabAttribute := mkElabAttribute `elabTerm "term" builtinTermElabTable
 @[init mkTermElabAttribute] constant termElabAttribute : TermElabAttribute := arbitrary _
 
-@[inline] def liftMetaM {α} (x : Meta.MetaM α) : TermElabM α :=
+@[inline] def liftMetaM {α} (x : MetaM α) : TermElabM α :=
 fun ctx s => match x ctx.toContext s.toState with
   | EStateM.Result.ok a newS     => EStateM.Result.ok a { toState := newS, .. s }
   | EStateM.Result.error ex newS => EStateM.Result.error (Exception.meta ex) { toState := newS, .. s }
@@ -88,6 +89,9 @@ fun ctx s => match x ctx.toContext s.toState with
 def isDefEq (t s : Expr) : TermElabM Bool := liftMetaM $ Meta.isDefEq t s
 def inferType (e : Expr) : TermElabM Expr := liftMetaM $ Meta.inferType e
 def whnf (e : Expr) : TermElabM Expr := liftMetaM $ Meta.whnf e
+def mkFreshLevelMVar : TermElabM Level := liftMetaM $ Meta.mkFreshLevelMVar
+def mkFreshExprMVar (type : Expr) (userName? : Name := Name.anonymous) (synthetic : Bool := false) : TermElabM Expr :=
+liftMetaM $ Meta.mkFreshExprMVar type userName? synthetic
 
 def elabTerm (stx : Syntax) (expectedType : Option Expr) : TermElabM Expr :=
 stx.ifNode
@@ -100,8 +104,14 @@ stx.ifNode
     | none      => throw $ Exception.other ("elaboration function for '" ++ toString k ++ "' has not been implemented"))
   (fun _ => throw $ Exception.other "term elaborator failed, unexpected syntax")
 
+def elabType (stx : Syntax) : TermElabM Expr :=
+do u ← mkFreshLevelMVar;
+   elabTerm stx (mkSort u)
+
 end Term
 
+export Term (TermElabM)
+
 /-
 partial def elabTermAux : Syntax Expr → Option Expr → Bool → Elab (Syntax Expr)
 | stx, expectedType, expanding => stx.ifNode
diff --git a/src/Init/Lean/Meta.lean b/src/Init/Lean/Meta.lean
index a0ba448e37..2ab077f223 100644
--- a/src/Init/Lean/Meta.lean
+++ b/src/Init/Lean/Meta.lean
@@ -17,3 +17,7 @@ import Init.Lean.Meta.AbstractMVars
 import Init.Lean.Meta.SynthInstance
 import Init.Lean.Meta.AppBuilder
 import Init.Lean.Meta.Tactic
+
+namespace Lean
+export Meta (MetaM)
+end Lean