diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 2a2224c8cd..90116861a9 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -279,14 +279,14 @@ let attrImpl : AttributeImpl := {
   name  := name,
   descr := descr,
   add   := fun decl args persistent => do
-    when args.hasArgs $ Core.throwError ("invalid attribute '" ++ toString name ++ "', unexpected argument");
-    unless persistent $ Core.throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
-    env ← Core.getEnv;
+    when args.hasArgs $ throwError ("invalid attribute '" ++ toString name ++ "', unexpected argument");
+    unless persistent $ throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
+    env ← getEnv;
     unless (env.getModuleIdxFor? decl).isNone $
-      Core.throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
+      throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
     validate decl;
-    env ← Core.getEnv;
-    Core.setEnv $ ext.addEntry env decl
+    env ← getEnv;
+    setEnv $ ext.addEntry env decl
 };
 registerBuiltinAttribute attrImpl;
 pure { attr := attrImpl, ext := ext }
@@ -332,14 +332,14 @@ let attrImpl : AttributeImpl := {
   descr := descr,
   applicationTime := appTime,
   add   := fun decl args persistent => do
-    unless persistent $ Core.throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
-    env ← Core.getEnv;
+    unless persistent $ throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
+    env ← getEnv;
     unless (env.getModuleIdxFor? decl).isNone $
-      Core.throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
+      throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
     val ← getParam decl args;
     let env' := ext.addEntry env (decl, val);
-    Core.setEnv env';
-    catch (afterSet decl val) (fun _ => Core.setEnv env)
+    setEnv env';
+    catch (afterSet decl val) (fun _ => setEnv env)
 };
 registerBuiltinAttribute attrImpl;
 pure { attr := attrImpl, ext := ext }
@@ -392,12 +392,12 @@ let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => {
   descr           := descr,
   applicationTime := applicationTime,
   add             := (fun decl args persistent => do
-    unless persistent $ Core.throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
-    env ← Core.getEnv;
+    unless persistent $ throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
+    env ← getEnv;
     unless (env.getModuleIdxFor? decl).isNone $
-      Core.throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
+      throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
     validate decl val;
-    Core.setEnv $ ext.addEntry env (decl, val))
+    setEnv $ ext.addEntry env (decl, val))
   : AttributeImpl
 };
 attrs.forM registerBuiltinAttribute;
diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index 28ad5746a3..bba81364a6 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -140,11 +140,11 @@ registerBuiltinAttribute {
   name  := `class,
   descr := "type class",
   add   := fun decl args persistent => do
-    env ← Core.getEnv;
-    when args.hasArgs $ Core.throwError "invalid attribute 'class', unexpected argument";
-    unless persistent $ Core.throwError "invalid attribute 'class', must be persistent";
-    env ← Core.ofExcept (addClass env decl);
-    Core.setEnv env
+    env ← getEnv;
+    when args.hasArgs $ throwError "invalid attribute 'class', unexpected argument";
+    unless persistent $ throwError "invalid attribute 'class', must be persistent";
+    env ← ofExcept (addClass env decl);
+    setEnv env
 }
 
 -- TODO: delete
diff --git a/src/Lean/Compiler/ExportAttr.lean b/src/Lean/Compiler/ExportAttr.lean
index 237797a6d7..6ec4b96c4b 100644
--- a/src/Lean/Compiler/ExportAttr.lean
+++ b/src/Lean/Compiler/ExportAttr.lean
@@ -21,8 +21,8 @@ registerParametricAttribute `export "name to be used by code generators" $ fun _
   match attrParamSyntaxToIdentifier stx with
   | some exportName =>
     if isValidCppName exportName then pure exportName
-    else Core.throwError "invalid 'export' function name, is not a valid C++ identifier"
-  | _ => Core.throwError "unexpected kind of argument"
+    else throwError "invalid 'export' function name, is not a valid C++ identifier"
+  | _ => throwError "unexpected kind of argument"
 
 @[init mkExportAttr]
 constant exportAttr : ParametricAttribute Name := arbitrary _
diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean
index d1594f227c..440d5b812c 100644
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.lean
@@ -80,12 +80,12 @@ constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environmen
 
 def mkExternAttr : IO (ParametricAttribute ExternAttrData) :=
 registerParametricAttribute `extern "builtin and foreign functions"
-  (fun _ stx => Core.ofExcept $ syntaxToExternAttrData stx)
+  (fun _ stx => ofExcept $ syntaxToExternAttrData stx)
   (fun declName _ => do
-    env ← Core.getEnv;
+    env ← getEnv;
     if env.isProjectionFn declName || env.isConstructor declName then do
-      env ← Core.ofExcept $ addExtern env declName;
-      Core.setEnv env
+      env ← ofExcept $ addExtern env declName;
+      setEnv env
     else
       pure ())
 
diff --git a/src/Lean/Compiler/IR/UnboxResult.lean b/src/Lean/Compiler/IR/UnboxResult.lean
index 483b5a862e..ec7de8284a 100644
--- a/src/Lean/Compiler/IR/UnboxResult.lean
+++ b/src/Lean/Compiler/IR/UnboxResult.lean
@@ -12,12 +12,12 @@ namespace UnboxResult
 
 def mkUnboxAttr : IO TagAttribute :=
 registerTagAttribute `unbox "compiler tries to unbox result values if their types are tagged with `[unbox]`" $ fun declName => do
-  cinfo ← Core.getConstInfo declName;
+  cinfo ← getConstInfo declName;
   match cinfo with
   | ConstantInfo.inductInfo v =>
-    if v.isRec then Core.throwError "recursive inductive datatypes are not supported"
+    if v.isRec then throwError "recursive inductive datatypes are not supported"
     else pure ()
-  | _ => Core.throwError "constant must be an inductive type"
+  | _ => throwError "constant must be an inductive type"
 
 @[init mkUnboxAttr]
 constant unboxAttr : TagAttribute := arbitrary _
diff --git a/src/Lean/Compiler/ImplementedByAttr.lean b/src/Lean/Compiler/ImplementedByAttr.lean
index a30ab9e023..4bd2f3c30b 100644
--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/src/Lean/Compiler/ImplementedByAttr.lean
@@ -10,13 +10,13 @@ namespace Compiler
 
 def mkImplementedByAttr : IO (ParametricAttribute Name) :=
 registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) function that implements opaque constant" fun declName stx => do
-  decl ← Core.getConstInfo declName;
+  decl ← getConstInfo declName;
   match attrParamSyntaxToIdentifier stx with
   | some fnName => do
-    fnDecl ← Core.getConstInfo fnName;
+    fnDecl ← getConstInfo fnName;
     if decl.type == fnDecl.type then pure fnName
-    else Core.throwError ("invalid function '" ++ fnName ++ "' type mismatch")
-  | _ => Core.throwError "expected identifier"
+    else throwError ("invalid function '" ++ fnName ++ "' type mismatch")
+  | _ => throwError "expected identifier"
 
 @[init mkImplementedByAttr]
 constant implementedByAttr : ParametricAttribute Name := arbitrary _
diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean
index 939a279337..c19ae21b86 100644
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -23,20 +23,20 @@ match getIOTypeArg type with
 
 def mkInitAttr : IO (ParametricAttribute Name) :=
 registerParametricAttribute `init "initialization procedure for global references" $ fun declName stx => do
-  decl ← Core.getConstInfo declName;
+  decl ← getConstInfo declName;
   match attrParamSyntaxToIdentifier stx with
   | some initFnName => do
-    initDecl ← Core.getConstInfo initFnName;
+    initDecl ← getConstInfo initFnName;
     match getIOTypeArg initDecl.type with
-    | none => Core.throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO <type>`")
+    | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO <type>`")
     | some initTypeArg =>
       if decl.type == initTypeArg then pure initFnName
-      else Core.throwError ("initialization function '" ++ initFnName ++ "' type mismatch")
+      else throwError ("initialization function '" ++ initFnName ++ "' type mismatch")
   | _ => match stx with
     | Syntax.missing =>
       if isIOUnit decl.type then pure Name.anonymous
-      else Core.throwError "initialization function must have type `IO Unit`"
-    | _ => Core.throwError "unexpected kind of argument"
+      else throwError "initialization function must have type `IO Unit`"
+    | _ => throwError "unexpected kind of argument"
 
 @[init mkInitAttr]
 constant initAttr : ParametricAttribute Name := arbitrary _
diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean
index 1975249874..92541a9ca9 100644
--- a/src/Lean/Compiler/InlineAttrs.lean
+++ b/src/Lean/Compiler/InlineAttrs.lean
@@ -34,8 +34,8 @@ registerEnumAttributes `inlineAttrs
    (`noinline, "mark definition to never be inlined", InlineAttributeKind.noinline),
    (`macroInline, "mark definition to always be inlined before ANF conversion", InlineAttributeKind.macroInline)]
   (fun declName _ => do
-    env ← Core.getEnv;
-    Core.ofExcept $ checkIsDefinition env declName)
+    env ← getEnv;
+    ofExcept $ checkIsDefinition env declName)
 
 @[init mkInlineAttrs]
 constant inlineAttrs : EnumAttributes InlineAttributeKind := arbitrary _
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 46716caeae..7f8eedde1f 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -11,6 +11,7 @@ import Lean.Environment
 import Lean.Exception
 import Lean.InternalExceptionId
 import Lean.Eval
+import Lean.MonadEnv
 
 namespace Lean
 namespace Core
@@ -33,8 +34,19 @@ abbrev CoreM := ReaderT Context $ StateRefT State $ EIO Exception
 instance CoreM.inhabited {α} : Inhabited (CoreM α) :=
 ⟨fun _ _ => throw $ arbitrary _⟩
 
-def getRef : CoreM Syntax := do
-ctx ← read; pure ctx.ref
+instance : MonadError CoreM :=
+{ getRef     := do ctx ← read; pure ctx.ref,
+  addContext := fun ref msg => do
+    ctx ← read;
+    s   ← get;
+    pure (ref, MessageData.withContext { env := s.env, mctx := {}, lctx := {}, opts := ctx.options } msg) }
+
+instance : MonadEnv CoreM :=
+{ getEnv    := do s ← get; pure s.env,
+  modifyEnv := fun f => modify fun s => { s with env := f s.env } }
+
+instance : MonadOptions CoreM :=
+{ getOptions := do ctx ← read; pure ctx.options }
 
 @[inline] def liftIOCore {α} (x : IO α) : CoreM α := do
 ref ← getRef;
@@ -43,21 +55,6 @@ liftM $ (adaptExcept (fun (err : IO.Error) => Exception.error ref (toString err)
 instance : MonadIO CoreM :=
 { liftIO := @liftIOCore }
 
-def addContext (msg : MessageData) : CoreM MessageData := do
-ctx ← read;
-s   ← get;
-pure $ MessageData.withContext { env := s.env, mctx := {}, lctx := {}, opts := ctx.options } msg
-
-def throwError {α} (msg : MessageData) : CoreM α := do
-ctx ← read;
-msg ← addContext msg;
-throw $ Exception.error ctx.ref msg
-
-def ofExcept {ε α} [HasToString ε] (x : Except ε α) : CoreM α :=
-match x with
-| Except.ok a    => pure a
-| Except.error e => throwError $ toString e
-
 def checkRecDepth : CoreM Unit := do
 ctx ← read;
 when (ctx.currRecDepth == ctx.maxRecDepth) $ throwError maxRecDepthErrorMessage
@@ -68,18 +65,6 @@ def Context.incCurrRecDepth (ctx : Context) : Context :=
 @[inline] def withIncRecDepth {α} (x : CoreM α) : CoreM α := do
 checkRecDepth; adaptReader Context.incCurrRecDepth x
 
-def getEnv : CoreM Environment := do
-s ← get; pure s.env
-
-def setEnv (env : Environment) : CoreM Unit :=
-modify $ fun s => { s with env := env }
-
-@[inline] def modifyEnv (f : Environment → Environment) : CoreM Unit :=
-modify $ fun s => { s with env := f s.env }
-
-def getOptions : CoreM Options :=  do
-ctx ← read; pure ctx.options
-
 def getTraceState : CoreM TraceState := do
 s ← get; pure s.traceState
 
@@ -98,11 +83,6 @@ let id := s.ngen.curr;
 modify $ fun s => { s with ngen := s.ngen.next };
 pure id
 
-def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
-match ref.getPos with
-| some _ => ref
-| _      => oldRef
-
 def Context.replaceRef (ref : Syntax) (ctx : Context) : Context :=
 { ctx with ref := replaceRef ref ctx.ref }
 
@@ -115,39 +95,9 @@ s ← get; pure s.traceState
 instance tracer : SimpleMonadTracerAdapter (CoreM) :=
 { getOptions       := getOptions,
   getTraceState    := getTraceState,
-  addContext       := addContext,
+  addContext       := fun msg => Prod.snd <$> addContext Syntax.missing msg,
   modifyTraceState := fun f => modify $ fun s => { s with traceState := f s.traceState } }
 
-def throwKernelException {α} (ex : KernelException) : CoreM α := do
-opts ← getOptions;
-throwError $ ex.toMessageData opts
-
-def addDecl (decl : Declaration) : CoreM Unit := do
-env ← getEnv;
-match env.addDecl decl with
-| Except.ok    env => setEnv env
-| Except.error ex  => throwKernelException ex
-
-def compileDecl (decl : Declaration) : CoreM Unit := do
-env  ← getEnv;
-opts ← getOptions;
-match env.compileDecl opts decl with
-| Except.ok env   => setEnv env
-| Except.error ex => throwKernelException ex
-
-def addAndCompile (decl : Declaration) : CoreM Unit := do
-addDecl decl;
-compileDecl decl
-
-def dbgTrace {α} [HasToString α] (a : α) : CoreM Unit :=
-_root_.dbgTrace (toString a) $ fun _ => pure ()
-
-def getConstInfo (constName : Name) : CoreM ConstantInfo := do
-env ← getEnv;
-match env.find? constName with
-| some info => pure info
-| none      => throwError ("unknown constant '" ++ constName ++ "'")
-
 def printTraces : CoreM Unit := do
 traceState ← getTraceState;
 traceState.traces.forM $ fun m => liftIO $ IO.println $ format m
diff --git a/src/Lean/Data/Options.lean b/src/Lean/Data/Options.lean
index be8a2306eb..2d6f8a43cc 100644
--- a/src/Lean/Data/Options.lean
+++ b/src/Lean/Data/Options.lean
@@ -90,4 +90,29 @@ registerOption `timeout { defValue := DataValue.ofNat 0, group := "", descr := "
 @[init] def maxMemoryOption : IO Unit :=
 registerOption `maxMemory { defValue := DataValue.ofNat 2048, group := "", descr := "maximum amount of memory available for Lean in megabytes" }
 
+class MonadOptions (m : Type → Type) :=
+(getOptions : m Options)
+
+export MonadOptions (getOptions)
+
+/- We currently cannot mark the following definition as an instance since it increases the search space too much -/
+def monadOptsFromLift (m) {n} [MonadOptions m] [HasMonadLiftT m n] : MonadOptions n :=
+{ getOptions := liftM (getOptions : m _) }
+
+instance ReaderT.monadOpts {ρ m} [MonadOptions m] : MonadOptions (ReaderT ρ m) := monadOptsFromLift m
+instance StateRefT.monadOpts {σ m} [MonadOptions m] : MonadOptions (StateRefT σ m) := monadOptsFromLift m
+
+section Methods
+
+variables {m : Type → Type} [Monad m] [MonadOptions m]
+
+def getBoolOption (k : Name) (defValue := false) : m Bool := do
+opts ← getOptions;
+pure $ opts.getBool k defValue
+
+def getNatOption (k : Name) (defValue := 0) : m Nat := do
+opts ← getOptions;
+pure $ opts.getNat k defValue
+
+end Methods
 end Lean
diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 2d9305217f..44a5652fe8 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -209,9 +209,6 @@ pure $ annotatePos ctx.pos stx
 @[inline] def liftMetaM {α} (x : MetaM α) : DelabM α :=
 liftM x
 
-def getEnv : DelabM Environment :=
-liftMetaM $ Meta.getEnv
-
 partial def delabFor : Name → Delab
 | k => do
   env ← getEnv;
@@ -430,7 +427,7 @@ e ← withProj delab;
 def delabProjectionApp : Delab := whenPPOption getPPStructureProjections $ do
 e@(Expr.app fn _ _) ← getExpr | failure;
 Expr.const c@(Name.str _ f _) _ _ ← pure fn.getAppFn | failure;
-env ← liftM getEnv;
+env ← getEnv;
 some info ← pure $ env.getProjectionFnInfo? c | failure;
 -- can't use with classes since the instance parameter is implicit
 guard $ !info.fromClass;
@@ -467,7 +464,7 @@ end Delaborator
 
 /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/
 def delab (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Syntax := do
-opts ← Meta.getOptions;
+opts ← getOptions;
 some stx ← Delaborator.delab { expr := e, defaultOptions := opts, optionsPerPos := optionsPerPos }
   | unreachable!;
 pure stx
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 96cca11882..de006785a3 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -52,6 +52,31 @@ abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
 abbrev CommandElabM := CommandElabCoreM Exception
 abbrev CommandElab  := Syntax → CommandElabM Unit
 
+instance : MonadEnv CommandElabM :=
+{ getEnv    := do s ← get; pure s.env,
+  modifyEnv := fun f => modify fun s => { s with env := f s.env } }
+
+instance : MonadOptions CommandElabM :=
+{ getOptions := do s ← get; pure s.scopes.head!.opts }
+
+protected def getRef : CommandElabM Syntax :=
+do ctx ← read; pure ctx.ref
+
+protected def addContext' (msg : MessageData) : CommandElabM MessageData := do
+env ← getEnv; opts ← getOptions;
+pure (MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msg)
+
+protected def addContext (ref : Syntax) (msg : MessageData) : CommandElabM (Syntax × MessageData) := do
+ctx ← read;
+let ref := getBetterRef ref ctx.macroStack;
+let msg := addMacroStack msg ctx.macroStack;
+msg ← Command.addContext' msg;
+pure (ref, msg)
+
+instance : MonadError CommandElabM :=
+{ getRef     := Command.getRef,
+  addContext := Command.addContext }
+
 def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
 mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
 
@@ -96,37 +121,16 @@ liftEIO $ adaptExcept (fun (ex : IO.Error) => Exception.error ctx.ref ex.toStrin
 instance : MonadIO CommandElabM :=
 { liftIO := fun α => liftIO }
 
-def getEnv : CommandElabM Environment := do s ← get; pure s.env
 def getScope : CommandElabM Scope := do s ← get; pure s.scopes.head!
-def getOptions : CommandElabM Options := do scope ← getScope; pure scope.opts
-
-def addContext (msg : MessageData) : CommandElabM MessageData := do
-env ← getEnv; opts ← getOptions;
-pure (MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msg)
 
 instance CommandElabM.monadLog : MonadLog CommandElabM :=
-{ getRef      := do ctx ← read; pure ctx.ref,
-  getFileMap  := do ctx ← read; pure ctx.fileMap,
+{ getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
-  addContext  := addContext,
+  addContext  := Command.addContext',
   logMessage  := fun msg => modify $ fun s => { s with messages := s.messages.add msg } }
 
-/--
-  Throws an error with the given `msgData` and extracting position information from `ref`.
-  If `ref` does not contain position information, then use `cmdPos` -/
-def throwError {α} (msgData : MessageData) : CommandElabM α := do
-ctx ← read;
-let ref     := getBetterRef ctx.ref ctx.macroStack;
-let msgData := addMacroStack msgData ctx.macroStack;
-msgData ← addContext msgData;
-withRef ref do
-  throw $ Exception.error ref msgData
-
-def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : CommandElabM α :=
-withRef ref $ throwError msgData
-
 def logTrace (cls : Name) (msg : MessageData) : CommandElabM Unit := do
-msg ← addContext $ MessageData.tagged cls msg;
+msg ← Command.addContext' $ MessageData.tagged cls msg;
 logInfo msg
 
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : CommandElabM Unit := do
@@ -173,7 +177,7 @@ instance : MonadMacroAdapter CommandElabM :=
   setNextMacroScope      := fun next => modify $ fun s => { s with nextMacroScope := next },
   getCurrRecDepth        := do ctx ← read; pure ctx.currRecDepth,
   getMaxRecDepth         := do s ← get; pure s.maxRecDepth,
-  throwError             := @throwErrorAt,
+  throwError             := fun α ref msg => throwErrorAt ref msg,
   throwUnsupportedSyntax := fun α => throwUnsupportedSyntax}
 
 partial def elabCommand : Syntax → CommandElabM Unit
@@ -261,12 +265,6 @@ fun ctx ref => EIO.catchExceptions (withLogging x ctx ref) (fun _ => pure ())
 def dbgTrace {α} [HasToString α] (a : α) : CommandElabM Unit :=
 _root_.dbgTrace (toString a) $ fun _ => pure ()
 
-def setEnv (newEnv : Environment) : CommandElabM Unit :=
-modify $ fun s => { s with env := newEnv }
-
-@[inline] def modifyEnv (f : Environment → Environment) : CommandElabM Unit :=
-modify $ fun s => { s with env := f s.env }
-
 def getCurrNamespace : CommandElabM Name := do
 scope ← getScope; pure scope.currNamespace
 
@@ -582,10 +580,10 @@ fun stx => withoutModifyingEnv do
             Term.mkLambda #[env, opts] e
           };
         addAndCompile e;
-        env ← Term.getEnv;
-        opts ← Term.getOptions;
+        env ← getEnv;
+        opts ← getOptions;
         match env.evalConst (Environment → Options → IO Environment) n with
-        | Except.error e => Term.throwError e
+        | Except.error e => throwError e
         | Except.ok act  => pure $ act env opts
     };
     (out, res) ← liftIO $ IO.Prim.withIsolatedStreams act;
@@ -602,9 +600,9 @@ fun stx => withoutModifyingEnv do
       Term.synthesizeSyntheticMVars false;
       e ← Term.mkAppM `Lean.HasEval.eval #[e, toExpr false];
       addAndCompile e;
-      env ← Term.getEnv;
+      env ← getEnv;
       match env.evalConst (IO Unit) n with
-      | Except.error e => Term.throwError e
+      | Except.error e => throwError e
       | Except.ok act  => pure act
     };
     (out, res) ← liftIO $ IO.Prim.withIsolatedStreams act;
diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index e2d94e45ec..5f82fbf09c 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -93,7 +93,7 @@ withDeclId declId $ fun name => do
     (type, _) ← Term.levelMVarToParam type;
     let usedParams  := (collectLevelParams {} type).params;
     match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams with
-    | Except.error msg      => Term.throwErrorAt stx msg
+    | Except.error msg      => throwErrorAt stx msg
     | Except.ok levelParams =>
       pure $ Declaration.axiomDecl {
         name     := declName,
diff --git a/src/Lean/Elab/Definition.lean b/src/Lean/Elab/Definition.lean
index 0b5278fcad..8141ddf362 100644
--- a/src/Lean/Elab/Definition.lean
+++ b/src/Lean/Elab/Definition.lean
@@ -88,7 +88,7 @@ else withUsedWhen vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun vars =>
   let usedParams  := collectLevelParams usedParams type;
   let usedParams  := collectLevelParams usedParams val;
   match sortDeclLevelParams scopeLevelNames allUserLevelNames usedParams.params with
-  | Except.error msg      => Term.throwError msg
+  | Except.error msg      => throwError msg
   | Except.ok levelParams =>
     match view.kind with
     | DefKind.theorem =>
@@ -102,7 +102,7 @@ else withUsedWhen vars xs val type view.kind.isDefOrAbbrevOrOpaque $ fun vars =>
         hints := ReducibilityHints.abbrev,
         isUnsafe := view.modifiers.isUnsafe }
     | DefKind.def => do
-      env ← Term.getEnv;
+      env ← getEnv;
       pure $ some $ Declaration.defnDecl {
         name := declName, lparams := levelParams, type := type, value := val,
         hints := ReducibilityHints.regular (getMaxHeight env val + 1),
@@ -115,7 +115,7 @@ if kind == `Lean.Parser.Command.declValSimple then
   -- parser! " := " >> termParser
   Term.elabTerm (defVal.getArg 1) expectedType
 else if kind == `Lean.Parser.Command.declValEqns then
-  Term.throwErrorAt defVal "equations have not been implemented yet"
+  throwErrorAt defVal "equations have not been implemented yet"
 else
   throwUnsupportedSyntax
 
diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 20f614b947..7f18152f86 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -87,7 +87,7 @@ private partial def elabHeaderAux (views : Array InductiveView)
       | some typeStx => do
         type ← Term.elabTerm typeStx none;
         unlessM (Term.isTypeFormerType type) $
-          Term.throwErrorAt typeStx "invalid inductive type, resultant type is not a sort";
+          throwErrorAt typeStx "invalid inductive type, resultant type is not a sort";
         elabHeaderAux (i+1) (acc.push { lctx := lctx, localInsts := localInsts, params := params, type := type, view := view })
   else
     pure acc
@@ -95,26 +95,26 @@ private partial def elabHeaderAux (views : Array InductiveView)
 private def checkNumParams (rs : Array ElabHeaderResult) : TermElabM Nat := do
 let numParams := (rs.get! 0).params.size;
 rs.forM fun r => unless (r.params.size == numParams) $
-  Term.throwErrorAt r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatypes";
+  throwErrorAt r.view.ref "invalid inductive type, number of parameters mismatch in mutually inductive datatypes";
 pure numParams
 
 private def checkUnsafe (rs : Array ElabHeaderResult) : TermElabM Unit :=
 let isUnsafe := (rs.get! 0).view.modifiers.isUnsafe;
 rs.forM fun r => unless (r.view.modifiers.isUnsafe == isUnsafe) $
-  Term.throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
+  throwErrorAt r.view.ref "invalid inductive type, cannot mix unsafe and safe declarations in a mutually inductive datatypes"
 
 private def checkLevelNames (views : Array InductiveView) : TermElabM Unit :=
 when (views.size > 1) do
   let levelNames := (views.get! 0).levelNames;
   views.forM fun view => unless (view.levelNames == levelNames) $
-    Term.throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
+    throwErrorAt view.ref "invalid inductive type, universe parameters mismatch in mutually inductive datatypes"
 
 private def mkTypeFor (r : ElabHeaderResult) : TermElabM Expr := do
 Term.withLocalContext r.lctx r.localInsts do
   Term.mkForall r.params r.type
 
 private def throwUnexpectedInductiveType {α} : TermElabM α :=
-Term.throwError "unexpected inductive resulting type"
+throwError "unexpected inductive resulting type"
 
 -- Given `e` of the form `forall As, B`, return `B`.
 private def getResultingType (e : Expr) : TermElabM Expr :=
@@ -134,15 +134,15 @@ private partial def checkParamsAndResultType (numParams : Nat) : Nat → Expr 
       unless (n₁ == n₂) $
         let msg : MessageData :=
           "invalid mutually inductive types, parameter name mismatch '" ++ n₁ ++ "', expected '" ++ n₂ ++ "'";
-        Term.throwError msg;
+        throwError msg;
       unlessM (Term.isDefEq d₁ d₂) $
         let msg : MessageData :=
           "invalid mutually inductive types, type mismatch at parameter '" ++ n₁ ++ "'" ++ indentExpr d₁
           ++ Format.line ++ "expected type" ++ indentExpr d₂;
-        Term.throwError msg;
+        throwError msg;
       unless (c₁.binderInfo == c₂.binderInfo) $
         -- TODO: improve this error message?
-        Term.throwError ("invalid mutually inductive types, binder annotation mismatch at parameter '" ++ n₁ ++ "'");
+        throwError ("invalid mutually inductive types, binder annotation mismatch at parameter '" ++ n₁ ++ "'");
       Term.withLocalDecl n₁ c₁.binderInfo d₁ fun x =>
         let type      := b₁.instantiate1 x;
         let firstType := b₂.instantiate1 x;
@@ -158,7 +158,7 @@ private partial def checkParamsAndResultType (numParams : Nat) : Nat → Expr 
       unlessM (Term.liftMetaM $ eqvFirstTypeResult firstType type) $
         let msg : MessageData :=
           "invalid mutually inductive types, resulting universe mismatch, given " ++ indentExpr type ++ Format.line ++ "expected type" ++ indentExpr firstType;
-        Term.throwError msg
+        throwError msg
     | _ => throwUnexpectedInductiveType
 
 -- Auxiliary function for checking whether the types in mutually inductive declaration are compatible.
@@ -230,15 +230,15 @@ r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getAr
   type ← match ctorView.type? with
     | none          => do
       when indFamily $
-        Term.throwError "constructor resulting type must be specified in inductive family declaration";
+        throwError "constructor resulting type must be specified in inductive family declaration";
       pure indFVar
     | some ctorType => do {
       type ← Term.elabTerm ctorType none;
       resultingType ← getResultingType type;
       unless (resultingType.getAppFn == indFVar) $
-        Term.throwError ("unexpected constructor resulting type" ++ indentExpr resultingType);
+        throwError ("unexpected constructor resulting type" ++ indentExpr resultingType);
       unlessM (Term.isType resultingType) $
-        Term.throwError ("unexpected constructor resulting type, type expected" ++ indentExpr resultingType);
+        throwError ("unexpected constructor resulting type, type expected" ++ indentExpr resultingType);
       pure type
     };
   type ← Term.mkForall ctorParams type;
@@ -261,12 +261,12 @@ private def levelMVarToParam (indTypes : List InductiveType) : TermElabM (List I
 (levelMVarToParamAux indTypes).run' 1
 
 private def getResultingUniverse : List InductiveType → TermElabM Level
-| []           => Term.throwError "unexpected empty inductive declaration"
+| []           => throwError "unexpected empty inductive declaration"
 | indType :: _ => do
   r ← getResultingType indType.type;
   match r with
   | Expr.sort u _ => pure u
-  | _             => Term.throwError "unexpected inductive type resulting type"
+  | _             => throwError "unexpected inductive type resulting type"
 
 def tmpIndParam := mkLevelParam `_tmp_ind_univ_param
 
@@ -282,7 +282,7 @@ if u.hasMVar then
     Term.assignLevelMVar mvarId tmpIndParam;
     pure true
   | _ =>
-    Term.throwError $
+    throwError $
       "cannot infer resulting universe level of inductive datatype, given level contains metavariables " ++ mkSort u ++ ", provide universe explicitly"
 else
   pure false
@@ -310,7 +310,7 @@ private partial def collectUniversesFromCtorTypeAux (r : Level) (rOffset : Nat)
   u ← Term.getLevel d;
   u ← Term.instantiateLevelMVars u;
   match accLevelAtCtor u r rOffset us with
-  | Except.error msg => Term.throwError msg
+  | Except.error msg => throwError msg
   | Except.ok us     => Term.withLocalDecl n c.binderInfo d $ fun x =>
     let e := b.instantiate1 x;
     collectUniversesFromCtorTypeAux 0 e us
@@ -338,7 +338,7 @@ r ← getResultingUniverse indTypes;
 let rOffset : Nat   := r.getOffset;
 let r       : Level := r.getLevelOffset;
 unless (r.isParam) $
-  Term.throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly";
+  throwError "failed to compute resulting universe level of inductive datatype, provide universe explicitly";
 us ← collectUniverses r rOffset numParams indTypes;
 let rNew := Level.mkNaryMax us.toList;
 pure $ indTypes.map fun indType =>
@@ -455,7 +455,7 @@ adaptReader (fun (ctx : Term.Context) => { ctx with levelNames := allUserLevelNa
       indTypes ← if inferLevel then updateResultingUniverse numParams indTypes else pure indTypes;
       let usedLevelNames := collectLevelParamsInInductive indTypes;
       match sortDeclLevelParams scopeLevelNames allUserLevelNames usedLevelNames with
-      | Except.error msg      => Term.throwError msg
+      | Except.error msg      => throwError msg
       | Except.ok levelParams => do
         indTypes ← replaceIndFVarsWithConsts views indFVars levelParams numParams indTypes;
         let indTypes := applyInferMod views numParams indTypes;
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index cb77711bf4..0e672bf50d 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -23,9 +23,12 @@ structure State :=
 
 abbrev LevelElabM := ReaderT Context (EStateM Exception State)
 
-instance LevelElabM.MonadLog : MonadPosInfo LevelElabM :=
+instance LevelElabM.monadError : MonadError LevelElabM :=
 { getRef      := do ctx ← read; pure ctx.ref,
-  getFileMap  := do ctx ← read; pure ctx.fileMap,
+  addContext  := fun ref msg => pure (ref, msg) }
+
+instance LevelElabM.monadLog : MonadPosInfo LevelElabM :=
+{ getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
   addContext  := fun msg => pure msg }
 
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index 60bf8edf9b..3791680a52 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -9,23 +9,19 @@ import Lean.Elab.Exception
 namespace Lean
 namespace Elab
 
-def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
-Core.replaceRef ref oldRef
-
 class MonadPosInfo (m : Type → Type) :=
 (getFileMap   : m FileMap)
 (getFileName  : m String)
-(getRef       : m Syntax)
 (addContext   : MessageData → m MessageData)
 
-export MonadPosInfo (getFileMap getFileName getRef)
+export MonadPosInfo (getFileMap getFileName)
 
 class MonadLog (m : Type → Type) extends MonadPosInfo m :=
 (logMessage   : Message → m Unit)
 
 export MonadLog (logMessage)
 
-variables {m : Type → Type} [Monad m]
+variables {m : Type → Type} [Monad m] [MonadError m]
 
 def getRefPos [MonadPosInfo m] : m String.Pos := do
 ref ← getRef;
@@ -67,9 +63,5 @@ log MessageSeverity.warning msgData
 def logInfo [MonadLog m] (msgData : MessageData) : m Unit :=
 log MessageSeverity.information msgData
 
-def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (msg : MessageData) : m α := do
-ref ← getRef;
-throw $ Exception.error ref msg
-
 end Elab
 end Lean
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index fcbdf393d3..2b19e2853f 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -165,10 +165,10 @@ structure State :=
 (found     : NameSet := {})
 (vars      : Array PatternVar := #[])
 
-abbrev M := StateT State TermElabM
+abbrev M := StateRefT State TermElabM
 
 private def throwCtorExpected {α} : M α :=
-liftM $ throwError "invalid pattern, constructor or constant marked with '[matchPattern]' expected"
+throwError "invalid pattern, constructor or constant marked with '[matchPattern]' expected"
 
 def withRef {α} (ref : Syntax) (x : M α) : M α :=
 adaptTheReader Core.Context (Core.Context.replaceRef ref) x
@@ -182,13 +182,13 @@ liftMetaM $ Meta.forallBoundedTelescope ctorVal.type ctorVal.nparams fun ps _ =>
     0
 
 private def throwAmbiguous {α} (fs : List Expr) : M α :=
-liftM $ throwError ("ambiguous pattern, use fully qualified name, possible interpretations " ++ fs)
+throwError ("ambiguous pattern, use fully qualified name, possible interpretations " ++ fs)
 
 private def processVar (id : Name) (mustBeCtor : Bool := false) : M Unit := do
 when mustBeCtor $ throwCtorExpected;
-unless id.eraseMacroScopes.isAtomic $ liftM $ throwError "invalid pattern variable, must be atomic";
+unless id.eraseMacroScopes.isAtomic $ throwError "invalid pattern variable, must be atomic";
 s ← get;
-when (s.found.contains id) $ liftM $ throwError ("invalid pattern, variable '" ++ id ++ "' occurred more than once");
+when (s.found.contains id) $ throwError ("invalid pattern, variable '" ++ id ++ "' occurred more than once");
 modify fun s => { s with vars := s.vars.push (PatternVar.localVar id), found := s.found.insert id }
 
 -- HACK: inlining this function crashes the compiler
@@ -209,7 +209,7 @@ match f with
    If `stx` is a constructor, then return the number of explicit arguments that are inductive type parameters. -/
 private def processIdAux (stx : Syntax) (mustBeCtor : Bool) : M Nat :=
 withRef stx do
-env ← liftM $ getEnv;
+env ← getEnv;
 match stx with
 | Syntax.ident _ _ val preresolved => do
   rs ← liftM $ catch (resolveName val preresolved []) (fun _ => pure []);
@@ -228,7 +228,7 @@ private def processId (stx : Syntax) : M Unit := do
 _ ← processIdAux stx false; pure ()
 
 private def throwInvalidPattern {α} : M α :=
-liftM $ throwError "invalid pattern"
+throwError "invalid pattern"
 
 private partial def collect : Syntax → M Syntax
 | stx@(Syntax.node k args) => withRef stx $ withFreshMacroScope $
@@ -237,7 +237,7 @@ private partial def collect : Syntax → M Syntax
     let appArgs := (args.get! 1).getArgs;
     appArgs.forM fun appArg =>
       when (appArg.isOfKind `Lean.Parser.Term.namedPattern) $
-        liftM $ throwErrorAt appArg "named parameters are not allowed in patterns";
+        throwErrorAt appArg "named parameters are not allowed in patterns";
     /- We must skip explict inducitve datatype parameters since they are by defaul inaccessible.
        Example: `A` is inaccessible term at `Sum.inl A b` -/
     numArgsToSkip ← processCtor appFn;
@@ -250,7 +250,7 @@ private partial def collect : Syntax → M Syntax
     /- { " >> optional (try (termParser >> " with ")) >> sepBy structInstField ", " true >> optional ".." >> optional (" : " >> termParser) >> " }" -/
     let withMod := args.get! 1;
     unless withMod.isNone $
-      liftM $ throwErrorAt withMod "invalid struct instance pattern, 'with' is not allowed in patterns";
+      throwErrorAt withMod "invalid struct instance pattern, 'with' is not allowed in patterns";
     let fields := (args.get! 2).getArgs;
     fields ← fields.mapSepElemsM fun field => do {
       -- parser! structInstLVal >> " := " >> termParser
@@ -305,7 +305,7 @@ private partial def collect : Syntax → M Syntax
   else if k == charLitKind then
     pure stx
   else if k == choiceKind then
-    liftM $ throwError "invalid pattern, notation is ambiguous"
+    throwError "invalid pattern, notation is ambiguous"
   else
     throwInvalidPattern
 | stx@(Syntax.ident _ _ _ _) => do
@@ -406,7 +406,7 @@ structure State :=
 (localDecls : Array LocalDecl)
 (newLocals  : NameSet := {})
 
-abbrev M := StateT State TermElabM
+abbrev M := StateRefT State TermElabM
 
 private def alreadyVisited (fvarId : FVarId) : M Bool := do
 s ← get;
@@ -416,7 +416,7 @@ private def markAsVisited (fvarId : FVarId) : M Unit :=
 modify $ fun s => { s with found := s.found.insert fvarId }
 
 private def throwInvalidPattern {α} (e : Expr) : M α :=
-liftM $ throwError ("invalid pattern " ++ indentExpr e)
+throwError ("invalid pattern " ++ indentExpr e)
 
 private def getFieldsBinderInfoAux (ctorVal : ConstructorVal) : Nat → Expr → Array BinderInfo → Array BinderInfo
 | i, Expr.forallE _ d b c, bis =>
@@ -485,7 +485,7 @@ partial def main : Expr → M Pattern
     p ← main $ e.getArg! 2;
     match e.getArg! 1 with
     | Expr.fvar fvarId _ => pure $ Pattern.as fvarId p
-    | _                  => liftM $ throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
+    | _                  => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
   else if e.isNatLit || e.isStringLit || e.isCharLit then
     pure $ Pattern.val e
   else if e.isFVar then do
@@ -500,7 +500,7 @@ partial def main : Expr → M Pattern
       main newE
     else match e.getAppFn with
       | Expr.const declName us _ => do
-        env ← liftM getEnv;
+        env ← getEnv;
         match env.find? declName with
         | ConstantInfo.ctorInfo v =>  do
           let args := e.getAppArgs;
diff --git a/src/Lean/Elab/StructInst.lean b/src/Lean/Elab/StructInst.lean
index 8356f0bc0c..b8f87fe41b 100644
--- a/src/Lean/Elab/StructInst.lean
+++ b/src/Lean/Elab/StructInst.lean
@@ -590,7 +590,7 @@ match field.lhs with
 | [FieldLHS.fieldName _ fieldName] => fieldName
 | _ => unreachable!
 
-abbrev M := ReaderT Context (StateT State TermElabM)
+abbrev M := ReaderT Context (StateRefT State TermElabM)
 
 def isRoundDone : M Bool := do
 ctx ← read;
@@ -634,7 +634,7 @@ def reduceProjOf? (structNames : Array Name) (e : Expr) : MetaM (Option Expr) :=
 if !e.isApp then pure none
 else match e.getAppFn with
   | Expr.const name _ _ => do
-    env ← Meta.getEnv;
+    env ← getEnv;
     match env.getProjectionStructureName? name with
     | some structName =>
       if structNames.contains structName then
@@ -733,7 +733,7 @@ partial def propagateLoop (hierarchyDepth : Nat) : Nat → Struct → M Unit
   | none       => pure () -- Done
   | some field =>
     if d > hierarchyDepth then
-      liftM $ throwErrorAt field.ref ("field '" ++ getFieldName field ++ "' is missing")
+      throwErrorAt field.ref ("field '" ++ getFieldName field ++ "' is missing")
     else adaptReader (fun (ctx : Context) => { ctx with maxDistance := d }) $ do
       modify $ fun (s : State) => { s with progress := false };
       step struct;
diff --git a/src/Lean/Elab/Structure.lean b/src/Lean/Elab/Structure.lean
index 0c508f2ea3..1a2bd73553 100644
--- a/src/Lean/Elab/Structure.lean
+++ b/src/Lean/Elab/Structure.lean
@@ -196,11 +196,11 @@ match type with
 private def checkParentIsStructure (parent : Expr) : TermElabM Name :=
 match parent.getAppFn with
 | Expr.const c _ _ => do
-  env ← Term.getEnv;
+  env ← getEnv;
   unless (isStructure env c) $
-    Term.throwError $ "'" ++ toString c ++ "' is not a structure";
+    throwError $ "'" ++ toString c ++ "' is not a structure";
   pure c
-| _ => Term.throwError $ "expected structure"
+| _ => throwError $ "expected structure"
 
 private def findFieldInfo? (infos : Array StructFieldInfo) (fieldName : Name) : Option StructFieldInfo :=
 infos.find? fun info => info.name == fieldName
@@ -213,9 +213,9 @@ private partial def processSubfields {α} (structDeclName : Name) (parentFVar :
 | i, infos, k =>
   if h : i < subfieldNames.size then do
     let subfieldName := subfieldNames.get ⟨i, h⟩;
-    env ← Term.getEnv;
+    env ← getEnv;
     when (containsFieldName infos subfieldName) $
-      Term.throwError ("field '" ++ subfieldName ++ "' from '" ++ parentStructName ++ "' has already been declared");
+      throwError ("field '" ++ subfieldName ++ "' from '" ++ parentStructName ++ "' has already been declared");
     val  ← Term.liftMetaM $ Meta.mkProjection parentFVar subfieldName;
     type ← Term.inferType val;
     Term.withLetDecl subfieldName type val fun subfieldFVar =>
@@ -236,8 +236,8 @@ private partial def withParents {α} (view : StructView) : Nat → Array StructF
     parentName ← checkParentIsStructure parent;
     let toParentName := mkNameSimple $ "to" ++ parentName.eraseMacroScopes.getString!; -- erase macro scopes?
     when (containsFieldName infos toParentName) $
-      Term.throwErrorAt parentStx ("field '" ++ toParentName ++ "' has already been declared");
-    env ← Term.getEnv;
+      throwErrorAt parentStx ("field '" ++ toParentName ++ "' has already been declared");
+    env ← getEnv;
     let binfo := if view.isClass && isClass env parentName then BinderInfo.instImplicit else BinderInfo.default;
     Term.withLocalDecl toParentName binfo parent $ fun parentFVar =>
       let infos := infos.push { name := toParentName, declName := view.declName ++ toParentName, fvar := parentFVar, kind := StructFieldKind.subobject };
@@ -274,7 +274,7 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
     | none      => do
       (type?, value?) ← Term.elabBinders view.binders.getArgs $ fun params => elabFieldTypeValue view params;
       match type?, value? with
-      | none,      none => Term.throwError "invalid field, type expected"
+      | none,      none => throwError "invalid field, type expected"
       | some type, _    =>
         Term.withLocalDecl view.name view.binderInfo type $ fun fieldFVar =>
           let infos := infos.push { name := view.name, declName := view.declName, fvar := fieldFVar, value? := value?,
@@ -287,13 +287,13 @@ private partial def withFields {α} (views : Array StructFieldView) : Nat → Ar
           withFields (i+1) infos k
     | some info =>
       match info.kind with
-      | StructFieldKind.newField   => Term.throwError ("field '" ++ view.name ++ "' has already been declared")
+      | StructFieldKind.newField   => throwError ("field '" ++ view.name ++ "' has already been declared")
       | StructFieldKind.fromParent =>
         match view.value? with
-        | none       => Term.throwError ("field '" ++ view.name ++ "' has been declared in parent structure")
+        | none       => throwError ("field '" ++ view.name ++ "' has been declared in parent structure")
         | some valStx => do
           when (!view.binders.getArgs.isEmpty || view.type?.isSome) $
-            Term.throwErrorAt view.type?.get! ("omit field '" ++ view.name ++ "' type to set default value");
+            throwErrorAt view.type?.get! ("omit field '" ++ view.name ++ "' type to set default value");
           fvarType ← Term.inferType info.fvar;
           value ← Term.elabTermEnsuringType valStx fvarType;
           let infos := infos.push { info with value? := value };
@@ -306,7 +306,7 @@ private def getResultUniverse (type : Expr) : TermElabM Level := do
 type ← Term.whnf type;
 match type with
 | Expr.sort u _ => pure u
-| _             => Term.throwError "unexpected structure resulting type"
+| _             => throwError "unexpected structure resulting type"
 
 private def removeUnused (scopeVars : Array Expr) (params : Array Expr) (fieldInfos : Array StructFieldInfo)
     : TermElabM (LocalContext × LocalInstances × Array Expr) := do
@@ -360,7 +360,7 @@ fieldInfos.foldlM
     u ← Term.getLevel type;
     u ← Term.instantiateLevelMVars u;
     match accLevelAtCtor u r rOffset us with
-    | Except.error msg => Term.throwError msg
+    | Except.error msg => throwError msg
     | Except.ok us     => pure us)
   #[]
 
@@ -374,7 +374,7 @@ match r with
   let rNew := Level.mkNaryMax us.toList;
   Term.assignLevelMVar mvarId rNew;
   Term.instantiateMVars type
-| _ => Term.throwError "failed to compute resulting universe level of structure, provide universe explicitly"
+| _ => throwError "failed to compute resulting universe level of structure, provide universe explicitly"
 
 private def collectLevelParamsInFVar (s : CollectLevelParams.State) (fvar : Expr) : TermElabM CollectLevelParams.State := do
 type ← Term.inferType fvar;
@@ -419,7 +419,7 @@ pure { name := view.ctor.declName, type := type }
 private def elabStructureView (view : StructView) : TermElabM ElabStructResult := do
 let numExplicitParams := view.params.size;
 type ← Term.elabType view.type;
-unless (validStructType type) $ Term.throwErrorAt view.type "expected Type";
+unless (validStructType type) $ throwErrorAt view.type "expected Type";
 Term.withRef view.ref do
 withParents view 0 #[] fun fieldInfos =>
 withFields view.fields 0 fieldInfos fun fieldInfos => do
@@ -432,7 +432,7 @@ withFields view.fields 0 fieldInfos fun fieldInfos => do
     type ← if inferLevel then updateResultingUniverse fieldInfos type else pure type;
     usedLevelNames ← collectLevelParamsInStructure scopeVars view.params fieldInfos;
     match sortDeclLevelParams view.scopeLevelNames view.allUserLevelNames usedLevelNames with
-    | Except.error msg      => Term.throwError msg
+    | Except.error msg      => throwError msg
     | Except.ok levelParams => do
       let params := scopeVars ++ view.params;
       ctor ← mkCtor view levelParams params fieldInfos;
@@ -496,7 +496,7 @@ liftTermElabM none $ Term.withLocalContext lctx localInsts do
     value ← Term.liftMetaM $ Meta.mkId value;
     let zeta := true; -- expand `let-declarations`
     _ ← Term.mkAuxDefinition declName type value zeta;
-    Term.modifyEnv fun env => setReducibilityStatus env declName ReducibilityStatus.reducible;
+    modifyEnv fun env => setReducibilityStatus env declName ReducibilityStatus.reducible;
     pure ()
 
 /-
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 75e50ef161..1eab7a9dd9 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -39,7 +39,7 @@ structure ToParserDescrContext :=
    See comment at `Parser.ParserCategory`. -/
 (leadingIdentAsSymbol : Bool)
 
-abbrev ToParserDescrM := ReaderT ToParserDescrContext (StateT Bool TermElabM)
+abbrev ToParserDescrM := ReaderT ToParserDescrContext (StateRefT Bool TermElabM)
 private def markAsTrailingParser : ToParserDescrM Unit := set true
 
 @[inline] private def withNotFirst {α} (x : ToParserDescrM α) : ToParserDescrM α :=
@@ -54,8 +54,8 @@ if ctx.first && stx.getKind == `Lean.Parser.Syntax.cat then do
   let cat := (stx.getIdAt 0).eraseMacroScopes;
   if cat == ctx.catName then do
     let prec? : Option Nat  := expandOptPrecedence (stx.getArg 1);
-    unless prec?.isNone $ liftM $ throwErrorAt (stx.getArg 1) ("invalid occurrence of ':<num>' modifier in head");
-    unless ctx.leftRec $ liftM $
+    unless prec?.isNone $ throwErrorAt (stx.getArg 1) ("invalid occurrence of ':<num>' modifier in head");
+    unless ctx.leftRec $
       throwErrorAt (stx.getArg 3) ("invalid occurrence of '" ++ cat ++ "', parser algorithm does not allow this form of left recursion");
     markAsTrailingParser; -- mark as trailing par
     pure true
@@ -71,7 +71,7 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
     let args := stx.getArgs;
     condM (checkLeftRec (stx.getArg 0))
       (do
-        when (args.size == 1) $ liftM $ throwErrorAt stx "invalid atomic left recursive syntax";
+        when (args.size == 1) $ throwErrorAt stx "invalid atomic left recursive syntax";
         let args := args.eraseIdx 0;
         args ← args.mapIdxM $ fun i arg => withNotFirst $ toParserDescrAux arg;
         liftM $ mkParserSeq args)
@@ -86,10 +86,10 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
     let cat := (stx.getIdAt 0).eraseMacroScopes;
     ctx ← read;
     if ctx.first && cat == ctx.catName then
-      liftM $ throwErrorAt stx "invalid atomic left recursive syntax"
+      throwErrorAt stx "invalid atomic left recursive syntax"
     else do
       let prec? : Option Nat  := expandOptPrecedence (stx.getArg 1);
-      env ← liftM getEnv;
+      env ← getEnv;
       if Parser.isParserCategory env cat then
         let prec := prec?.getD 0;
         `(ParserDescr.cat $(quote cat) $(quote prec))
@@ -109,11 +109,11 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
               | _                                          => false;
          let candidates := candidates.map fun ⟨c, _⟩ => c;
          match candidates with
-         | []  => liftM $ throwErrorAt (stx.getArg 3) ("unknown category '" ++ cat ++ "' or parser declaration")
+         | []  => throwErrorAt (stx.getArg 3) ("unknown category '" ++ cat ++ "' or parser declaration")
          | [c] => do
-           unless prec?.isNone $ liftM $ throwErrorAt (stx.getArg 3) "unexpected precedence";
+           unless prec?.isNone $ throwErrorAt (stx.getArg 3) "unexpected precedence";
            `(ParserDescr.parser $(quote c))
-         | cs  => liftM $ throwErrorAt (stx.getArg 3) ("ambiguous parser declaration " ++ toString cs)
+         | cs  => throwErrorAt (stx.getArg 3) ("ambiguous parser declaration " ++ toString cs)
   else if kind == `Lean.Parser.Syntax.atom then do
     match (stx.getArg 0).isStrLit? with
     | some atom => do
@@ -159,7 +159,7 @@ partial def toParserDescrAux : Syntax → ToParserDescrM Syntax
     d₂ ← withoutLeftRec $ toParserDescrAux (stx.getArg 2);
     `(ParserDescr.orelse $d₁ $d₂)
   else
-    liftM $ throwErrorAt stx $ "unexpected syntax kind of category `syntax`: " ++ kind
+    throwErrorAt stx $ "unexpected syntax kind of category `syntax`: " ++ kind
 
 /--
   Given a `stx` of category `syntax`, return a pair `(newStx, trailingParser)`,
@@ -436,7 +436,7 @@ pure ()
 @[inline] def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do
 Term.tryPostponeIfNoneOrMVar expectedType?;
 some expectedType ← pure expectedType?
-  | Term.throwError "expected type must be known";
+  | throwError "expected type must be known";
 x expectedType
 
 /-
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 1493c23b9f..26bfb43162 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -21,7 +21,7 @@ MessageData.joinSep (goals.map $ MessageData.ofGoal) (Format.line ++ Format.line
 def Term.reportUnsolvedGoals (goals : List MVarId) : TermElabM Unit := do
 ref ← getRef;
 let tailRef := ref.getTailWithPos.getD ref;
-Term.throwErrorAt tailRef $ "unsolved goals" ++ Format.line ++ goalsToMessageData goals
+throwErrorAt tailRef $ "unsolved goals" ++ Format.line ++ goalsToMessageData goals
 
 namespace Tactic
 
@@ -41,14 +41,11 @@ structure BacktrackableState :=
 abbrev TacticM := ReaderT Context $ StateRefT State $ TermElabM
 abbrev Tactic  := Syntax → TacticM Unit
 
-def getEnv : TacticM Environment := do s ← getThe Core.State; pure s.env
 def getMCtx : TacticM MetavarContext := do s ← getThe Meta.State; pure s.mctx
 def getLCtx : TacticM LocalContext := do ctx ← readThe Meta.Context; pure ctx.lctx
 def getLocalInsts : TacticM LocalInstances := do ctx ← readThe Meta.Context; pure ctx.localInstances
-def getOptions : TacticM Options := do ctx ← readThe Core.Context; pure ctx.options
 def getMVarDecl (mvarId : MVarId) : TacticM MetavarDecl := do mctx ← getMCtx; pure $ mctx.getDecl mvarId
 
-def setEnv (env : Environment) : TacticM Unit := modifyThe Core.State fun s => { s with env := env }
 def setMCtx (mctx : MetavarContext) : TacticM Unit := modifyThe Meta.State fun s => { s with mctx := mctx }
 
 @[inline] def modifyMCtx (f : MetavarContext → MetavarContext) : TacticM Unit := modifyThe Meta.State $ fun s => { s with mctx := f s.mctx }
@@ -102,7 +99,6 @@ liftM x
 liftTermElabM $ Term.liftMetaM x
 
 def instantiateMVars (e : Expr) : TacticM Expr := liftTermElabM $ Term.instantiateMVars e
-def addContext (msg : MessageData) : TacticM MessageData := liftTermElabM $ Term.addContext msg
 def isExprMVarAssigned (mvarId : MVarId) : TacticM Bool := liftTermElabM $ Term.isExprMVarAssigned mvarId
 def assignExprMVar (mvarId : MVarId) (val : Expr) : TacticM Unit := liftTermElabM $ Term.assignExprMVar mvarId val
 def ensureHasType (expectedType? : Option Expr) (e : Expr) : TacticM Expr := liftTermElabM $ Term.ensureHasType expectedType? e
@@ -123,18 +119,11 @@ let s := Lean.collectMVars {} e;
 pure s.result.toList
 
 instance monadLog : MonadLog TacticM :=
-{ getRef      := liftTermElabM getRef,
-  getFileMap  := liftTermElabM getFileMap,
+{ getFileMap  := liftTermElabM getFileMap,
   getFileName := liftTermElabM getFileName,
-  addContext  := addContext,
+  addContext  := fun msg => Prod.snd <$> addContext Syntax.missing msg,
   logMessage  := fun msg => liftTermElabM $ logMessage msg }
 
-def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : TacticM α := do
-liftTermElabM $ Term.throwErrorAt ref msgData
-
-def throwError {α} (msgData : MessageData) : TacticM α := do
-liftTermElabM $ Term.throwError msgData
-
 def checkRecDepth : TacticM Unit :=
 liftTermElabM $ Term.checkRecDepth
 
@@ -191,7 +180,7 @@ instance : MonadMacroAdapter TacticM :=
   setNextMacroScope      := fun next => modifyThe Term.State $ fun s => { s with nextMacroScope := next },
   getCurrRecDepth        := do ctx ← readThe Core.Context; pure ctx.currRecDepth,
   getMaxRecDepth         := do ctx ← readThe Core.Context; pure ctx.maxRecDepth,
-  throwError             := @throwErrorAt,
+  throwError             := fun α ref msg => throwErrorAt ref msg,
   throwUnsupportedSyntax := fun α => throwUnsupportedSyntax }
 
 @[specialize] private def expandTacticMacroFns (evalTactic : Syntax → TacticM Unit) (stx : Syntax) : List Macro → TacticM Unit
diff --git a/src/Lean/Elab/Tactic/Generalize.lean b/src/Lean/Elab/Tactic/Generalize.lean
index 8186a15c0c..f0090979ea 100644
--- a/src/Lean/Elab/Tactic/Generalize.lean
+++ b/src/Lean/Elab/Tactic/Generalize.lean
@@ -43,7 +43,7 @@ liftMetaTactic $ fun mvarId => do
     let eq     := mkApp3 (Lean.mkConst `Eq [u]) eType e (mkBVar 0);
     let target := Lean.mkForall x BinderInfo.default eType $ Lean.mkForall h BinderInfo.default eq (b.liftLooseBVars 0 1);
     evalGeneralizeFinalize mvarId e target
-  | _ => Meta.throwError "unexpected type after generalize"
+  | _ => throwError "unexpected type after generalize"
 
 -- If generalizing fails, fall back to not replacing anything
 private def evalGeneralizeFallback (h : Name) (e : Expr) (x : Name) : TacticM Unit :=
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index c51062d171..7fbc44d497 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -108,7 +108,7 @@ liftMetaMAtMain $ fun mvarId => do
   majorType ← Meta.whnf majorType;
   match majorType.getAppFn with
   | Expr.const n _ _ => do
-    env ← Meta.getEnv;
+    env ← getEnv;
     match env.find? n with
     | ConstantInfo.inductInfo val => pure val
     | _ => Meta.throwTacticEx `induction mvarId ("major premise type is not an inductive type " ++ indentExpr majorType)
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 223d785765..35f6c72648 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -120,9 +120,6 @@ match result with
 | EStateM.Result.ok e s     => do s.restore; pure e
 | EStateM.Result.error ex s => do s.restore; throw ex
 
-private def getRefImpl : TermElabM Syntax :=
-liftM $ Core.getRef
-
 /-- Auxiliary function for `liftMetaM` -/
 private def mkMessageAux (ref : Syntax) (ctx : Context) (msgData : MessageData) (severity : MessageSeverity) : Message :=
 let pos := ref.getPos.getD 0;
@@ -142,7 +139,7 @@ liftMetaMCore $ Meta.setTraceState s
 
 private def saveTraceAsMessages (traceState : TraceState) : TermElabM Unit :=
 unless traceState.traces.isEmpty do
-  ref ← getRefImpl;
+  ref ← getRef;
   ctx ← read;
   modify fun s =>
     { s with messages := traceState.traces.foldl
@@ -162,11 +159,9 @@ finally (liftMetaMCore x) (liftMetaMFinalizer oldTraceState)
 @[inline] def liftCoreM {α} (x : CoreM α) : TermElabM α :=
 liftMetaM $ liftM x
 
-def getEnv : TermElabM Environment := do s ← getThe Core.State; pure s.env
 def getMCtx : TermElabM MetavarContext := do s ← getThe Meta.State; pure s.mctx
 def getLCtx : TermElabM LocalContext := do ctx ← readThe Meta.Context; pure ctx.lctx
 def getLocalInsts : TermElabM LocalInstances := do ctx ← readThe Meta.Context; pure ctx.localInstances
-def getOptions : TermElabM Options := do ctx ← readThe Core.Context; pure ctx.options
 def getNGen : TermElabM NameGenerator := do s ← getThe Core.State; pure s.ngen
 def getLevelNames : TermElabM (List Name) := do ctx ← read; pure ctx.levelNames
 def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
@@ -176,38 +171,32 @@ def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
   | none   => unreachable!
 def getMessageLog : TermElabM MessageLog := do s ← get; pure s.messages
 
-def setEnv (env : Environment) : TermElabM Unit := modifyThe Core.State $ fun s => { s with env := env }
-@[inline] def modifyEnv (f : Environment → Environment) : TermElabM Unit := modifyThe Core.State $ fun s => { s with env := f s.env }
 def setMCtx (mctx : MetavarContext) : TermElabM Unit := modifyThe Meta.State $ fun s => { s with mctx := mctx }
 def setNGen (ngen : NameGenerator) : TermElabM Unit := modifyThe Core.State $ fun s => { s with ngen := ngen }
 
-def addContext (msg : MessageData) : TermElabM MessageData := do
+private def addContext' (msg : MessageData) : TermElabM MessageData := do
 env ← getEnv; mctx ← getMCtx; lctx ← getLCtx; opts ← getOptions;
 pure (MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msg)
 
+instance MonadError : MonadError TermElabM :=
+{ getRef     := getRef,
+  addContext := fun ref msg => do
+    ctx ← read;
+    let ref := getBetterRef ref ctx.macroStack;
+    let msg := if ctx.macroStackAtErr then addMacroStack msg ctx.macroStack else msg;
+    msg ← addContext' msg;
+    pure (ref, msg) }
+
 instance monadLog : MonadLog TermElabM :=
-{ getRef      := getRefImpl,
-  getFileMap  := do ctx ← read; pure ctx.fileMap,
+{ getFileMap  := do ctx ← read; pure ctx.fileMap,
   getFileName := do ctx ← read; pure ctx.fileName,
-  addContext  := addContext,
+  addContext  := addContext',
   logMessage  := fun msg => modify $ fun s => { s with messages := s.messages.add msg } }
 
 /- Execute `x` using using `ref` as the default Syntax for providing position information to error messages. -/
 @[inline] def withRef {α} (ref : Syntax) (x : TermElabM α) : TermElabM α := do
 adaptTheReader Core.Context (Core.Context.replaceRef ref) x
 
-/-- Throws an error with the given `msgData` and extracting position information from `ctx.ref`. -/
-def throwError {α} (msg : MessageData) : TermElabM α := do
-ctx ← read;
-ref ← getRef;
-let ref := getBetterRef ref ctx.macroStack;
-let msg := if ctx.macroStackAtErr then addMacroStack msg ctx.macroStack else msg;
-msg ← addContext msg;
-throw $ Exception.error ref msg
-
-def throwErrorAt {α} (ref : Syntax) (msgData : MessageData) : TermElabM α :=
-withRef ref $ throwError msgData
-
 def checkRecDepth : TermElabM Unit :=
 liftMetaM $ Meta.checkRecDepth
 
@@ -853,7 +842,7 @@ instance : MonadMacroAdapter TermElabM :=
   setNextMacroScope      := fun next => modify $ fun s => { s with nextMacroScope := next },
   getCurrRecDepth        := do ctx ← readThe Core.Context; pure ctx.currRecDepth,
   getMaxRecDepth         := do ctx ← readThe Core.Context; pure ctx.maxRecDepth,
-  throwError             := @throwErrorAt,
+  throwError             := fun α ref msg => throwErrorAt ref msg,
   throwUnsupportedSyntax := fun α => throwUnsupportedSyntax}
 
 private def isExplicit (stx : Syntax) : Bool :=
diff --git a/src/Lean/Environment.lean b/src/Lean/Environment.lean
index c3613e4899..71271cafb3 100644
--- a/src/Lean/Environment.lean
+++ b/src/Lean/Environment.lean
@@ -694,5 +694,4 @@ constant isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool :
 constant whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Expr := arbitrary _
 
 end Kernel
-
 end Lean
diff --git a/src/Lean/Exception.lean b/src/Lean/Exception.lean
index f72f54614b..0d63459cce 100644
--- a/src/Lean/Exception.lean
+++ b/src/Lean/Exception.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Message
 import Lean.InternalExceptionId
+import Lean.Data.Options
 
 namespace Lean
 
@@ -23,4 +24,47 @@ def Exception.getRef : Exception → Syntax
 
 instance Exception.inhabited : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
 
+class MonadError (m : Type → Type) extends MonadExceptOf Exception m :=
+(getRef     : m Syntax)
+(addContext : Syntax → MessageData → m (Syntax × MessageData))
+
+export MonadError (getRef addContext)
+
+instance ReaderT.monadError {ρ m} [Monad m] [MonadError m] : MonadError (ReaderT ρ m) :=
+{ getRef        := fun _ => getRef,
+  addContext    := fun ref msg _ => addContext ref msg }
+
+instance StateRefT.monadError {σ m} [Monad m] [MonadError m] : MonadError (StateRefT σ m) :=
+inferInstanceAs (MonadError (ReaderT _ _))
+
+section Methods
+
+variables {m : Type → Type} [Monad m] [MonadError m]
+
+def throwError {α} (msg : MessageData) : m α := do
+ref ← getRef;
+(ref, msg) ← addContext ref msg;
+throw $ Exception.error ref msg
+
+def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
+match ref.getPos with
+| some _ => ref
+| _      => oldRef
+
+def throwErrorAt {α} (ref : Syntax) (msg : MessageData) : m α := do
+ctxRef ← getRef;
+let ref := replaceRef ref ctxRef;
+(ref, msg) ← addContext ref msg;
+throw $ Exception.error ref msg
+
+def ofExcept {ε α} [HasToString ε] (x : Except ε α) : m α :=
+match x with
+| Except.ok a    => pure a
+| Except.error e => throwError $ toString e
+
+def throwKernelException {α} [MonadOptions m] (ex : KernelException) : m α := do
+opts ← getOptions;
+throwError $ ex.toMessageData opts
+
+end Methods
 end Lean
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index 20e3695e39..e8aaaa3685 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -131,17 +131,17 @@ registerBuiltinAttribute {
   name  := df.builtinName,
   descr := "(builtin) " ++ df.descr,
   add   := fun declName arg persistent => do {
-    env ← Core.getEnv;
-    unless persistent $ Core.throwError ("invalid attribute '" ++ df.builtinName ++ "', must be persistent");
-    key ← Core.ofExcept $ df.evalKey true env arg;
-    decl ← Core.getConstInfo declName;
+    env ← getEnv;
+    unless persistent $ throwError ("invalid attribute '" ++ df.builtinName ++ "', must be persistent");
+    key ← ofExcept $ df.evalKey true env arg;
+    decl ← getConstInfo declName;
     match decl.type with
     | Expr.const c _ _ =>
-      if c != df.valueTypeName then Core.throwError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected")
+      if c != df.valueTypeName then throwError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected")
       else do
         env ← liftIO $ declareBuiltin df attrDeclName env key declName;
-        Core.setEnv env
-    | _ => Core.throwError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected")
+        setEnv env
+    | _ => throwError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected")
   },
   applicationTime := AttributeApplicationTime.afterCompilation
 };
@@ -149,10 +149,10 @@ registerBuiltinAttribute {
   name            := df.name,
   descr           := df.descr,
   add             := fun constName arg persistent => do
-    env ← Core.getEnv;
-    key ← Core.ofExcept $ df.evalKey false env arg;
-    val ← Core.ofExcept $ env.evalConstCheck γ df.valueTypeName constName;
-    Core.setEnv $ ext.addEntry env { key := key, decl := constName, value := val },
+    env ← getEnv;
+    key ← ofExcept $ df.evalKey false env arg;
+    val ← ofExcept $ env.evalConstCheck γ df.valueTypeName constName;
+    setEnv $ ext.addEntry env { key := key, decl := constName, value := val },
   applicationTime := AttributeApplicationTime.afterCompilation
 };
 pure { defn := df, tableRef := tableRef, ext := ext }
diff --git a/src/Lean/Meta/Basic.lean b/src/Lean/Meta/Basic.lean
index 7f71cb88a9..6f178c0c18 100644
--- a/src/Lean/Meta/Basic.lean
+++ b/src/Lean/Meta/Basic.lean
@@ -141,9 +141,6 @@ instance : MonadIO MetaM :=
 instance MetaM.inhabited {α} : Inhabited (MetaM α) :=
 ⟨fun _ _ => arbitrary _⟩
 
-def getRef : MetaM Syntax :=
-liftM Core.getRef
-
 def addContext (msg : MessageData) : MetaM MessageData := do
 ctxCore ← readThe Core.Context;
 sCore   ← getThe Core.State;
@@ -151,10 +148,9 @@ ctx     ← read;
 s       ← get;
 pure $ MessageData.withContext { env := sCore.env, mctx := s.mctx, lctx := ctx.lctx, opts := ctxCore.options } msg
 
-def throwError {α} (msg : MessageData) : MetaM α := do
-ref ← getRef;
-msg ← addContext msg;
-throw $ Exception.error ref msg
+instance meta.monadError : MonadError MetaM :=
+{ getRef     := liftM (getRef : CoreM Syntax),
+  addContext := fun ref msg => do msg ← addContext msg; pure (ref, msg) }
 
 def throwIsDefEqStuck {α} : MetaM α :=
 throw $ Exception.internal isDefEqStuckExceptionId
@@ -183,15 +179,6 @@ s ← get; pure s.mctx
 def setMCtx (mctx : MetavarContext) : MetaM Unit :=
 modify $ fun s => { s with mctx := mctx }
 
-@[inline] def getOptions : MetaM Options :=
-liftM Core.getOptions
-
-@[inline] def getEnv : MetaM Environment :=
-liftM Core.getEnv
-
-def setEnv (env : Environment) : MetaM Unit :=
-liftM $ Core.setEnv env
-
 def getNGen : MetaM NameGenerator :=
 liftM Core.getNGen
 
@@ -279,9 +266,6 @@ mvarId ← mkFreshId;
 modify $ fun s => { s with mctx := s.mctx.addLevelMVarDecl mvarId };
 pure $ mkLevelMVar mvarId
 
-@[inline] def ofExcept {α ε} [HasToString ε] (x : Except ε α) : MetaM α :=
-liftM $ Core.ofExcept x
-
 @[inline] def shouldReduceAll : MetaM Bool := do
 ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all
 
@@ -378,12 +362,6 @@ match env.find? constName with
 | some info => pure (some info)
 | none      => throwUnknownConstant constName
 
-def getConstInfo (constName : Name) : MetaM ConstantInfo := do
-env ← getEnv;
-match env.find? constName with
-| some info => pure info
-| none      => throwUnknownConstant constName
-
 def getConstNoEx? (constName : Name) : MetaM (Option ConstantInfo) := do
 env ← getEnv;
 match env.find? constName with
@@ -877,7 +855,7 @@ opts  ← getOptions;
 mctx  ← getMCtx;
 lctx  ← getLCtx;
 match Lean.mkAuxDefinition env opts mctx lctx name type value with
-| Except.error ex          => liftM $ Core.throwKernelException ex
+| Except.error ex          => throwKernelException ex
 | Except.ok (e, env, mctx) => do setEnv env; setMCtx mctx; pure e
 
 /-- Similar to `mkAuxDefinition`, but infers the type of `value`. -/
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index 6bd1edd493..a3111545fb 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -47,12 +47,12 @@ registerBuiltinAttribute {
   name  := `instance,
   descr := "type class instance",
   add   := fun declName args persistent => do
-    when args.hasArgs $ Core.throwError "invalid attribute 'instance', unexpected argument";
-    unless persistent $ Core.throwError "invalid attribute 'instance', must be persistent";
-    env ← Core.getEnv;
-    env ← Core.ofExcept (addGlobalInstanceOld env declName); -- TODO: delete
+    when args.hasArgs $ throwError "invalid attribute 'instance', unexpected argument";
+    unless persistent $ throwError "invalid attribute 'instance', must be persistent";
+    env ← getEnv;
+    env ← ofExcept (addGlobalInstanceOld env declName); -- TODO: delete
     env ← liftIO $ addGlobalInstance env declName;
-    Core.setEnv env
+    setEnv env
 }
 
 end Meta
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index 438622d79f..8e050b5942 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -289,7 +289,7 @@ match cinfo with
 
 def mkRecursorAttr : IO (ParametricAttribute Nat) :=
 registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
-  (fun _ stx => Core.ofExcept $ syntaxToMajorPos stx)
+  (fun _ stx => ofExcept $ syntaxToMajorPos stx)
   (fun declName majorPos => do
     (mkRecursorInfoCore declName (some majorPos)).run';
     pure ())
diff --git a/src/Lean/MonadEnv.lean b/src/Lean/MonadEnv.lean
new file mode 100644
index 0000000000..1fb523f710
--- /dev/null
+++ b/src/Lean/MonadEnv.lean
@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Init.Control.Option
+import Lean.Environment
+import Lean.Exception
+
+namespace Lean
+
+class MonadEnv (m : Type → Type) :=
+(getEnv    : m Environment)
+(modifyEnv : (Environment → Environment) → m Unit)
+
+export MonadEnv (getEnv modifyEnv)
+
+/- We currently cannot mark the following definition as an instance since it increases the search space too much -/
+def monadEnvFromLift (m) {n} [MonadEnv m] [HasMonadLiftT m n] : MonadEnv n :=
+{ getEnv    := liftM (getEnv : m Environment),
+  modifyEnv := fun f => liftM (modifyEnv f : m Unit) }
+
+instance ReaderT.monadEnv {m ρ} [Monad m] [MonadEnv m] : MonadEnv (ReaderT ρ m) := monadEnvFromLift m
+instance StateRefT.monadEnv {m σ} [MonadEnv m] : MonadEnv (StateRefT σ m)   := monadEnvFromLift m
+instance OptionT.monadEnv {m} [Monad m] [MonadEnv m] : MonadEnv (OptionT m) := monadEnvFromLift m
+
+section Methods
+
+variables {m : Type → Type} [MonadEnv m]
+
+def setEnv (env : Environment) : m Unit :=
+modifyEnv fun _ => env
+
+section
+variables [Monad m] [MonadError m]
+
+def getConstInfo (constName : Name) : m ConstantInfo := do
+env ← getEnv;
+match env.find? constName with
+| some info => pure info
+| none      => throwError ("unknown constant '" ++ constName ++ "'")
+
+def addDecl [MonadOptions m] (decl : Declaration) : m Unit := do
+env ← getEnv;
+match env.addDecl decl with
+| Except.ok    env => setEnv env
+| Except.error ex  => throwKernelException ex
+
+def compileDecl [MonadOptions m] (decl : Declaration) : m Unit := do
+env  ← getEnv;
+opts ← getOptions;
+match env.compileDecl opts decl with
+| Except.ok env   => setEnv env
+| Except.error ex => throwKernelException ex
+
+def addAndCompile [MonadOptions m] (decl : Declaration) : m Unit := do
+addDecl decl;
+compileDecl decl
+
+end
+
+end Methods
+end Lean
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index e621476736..ef5f5c232f 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -373,18 +373,18 @@ declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParser catName declName
 
 private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
     (declName : Name) (args : Syntax) (persistent : Bool) : CoreM Unit := do
-when args.hasArgs $ Core.throwError ("invalid attribute '" ++ attrName ++ "', unexpected argument");
-unless persistent $ Core.throwError ("invalid attribute '" ++ attrName ++ "', must be persistent");
-decl ← Core.getConstInfo declName;
-env ← Core.getEnv;
+when args.hasArgs $ throwError ("invalid attribute '" ++ attrName ++ "', unexpected argument");
+unless persistent $ throwError ("invalid attribute '" ++ attrName ++ "', must be persistent");
+decl ← getConstInfo declName;
+env ← getEnv;
 match decl.type with
 | Expr.const `Lean.Parser.TrailingParser _ _ => do
   env ← liftIO $ declareTrailingBuiltinParser env catName declName;
-  Core.setEnv env
+  setEnv env
 | Expr.const `Lean.Parser.Parser _ _ => do
   env ← liftIO $ declareLeadingBuiltinParser env catName declName;
-  Core.setEnv env
-| _ => Core.throwError ("unexpected parser type at '" ++ declName ++ "' (`Parser` or `TrailingParser` expected");
+  setEnv env
+| _ => throwError ("unexpected parser type at '" ++ declName ++ "' (`Parser` or `TrailingParser` expected");
 runParserAttributeHooks catName declName /- builtin -/ true
 
 /-
@@ -400,26 +400,26 @@ registerBuiltinAttribute {
 }
 
 private def ParserAttribute.add (attrName : Name) (catName : Name) (declName : Name) (args : Syntax) (persistent : Bool) : CoreM Unit := do
-when args.hasArgs $ Core.throwError ("invalid attribute '" ++ attrName ++ "', unexpected argument");
-env ← Core.getEnv;
+when args.hasArgs $ throwError ("invalid attribute '" ++ attrName ++ "', unexpected argument");
+env ← getEnv;
 let categories := (parserExtension.getState env).categories;
 match mkParserOfConstant env categories declName with
-| Except.error ex => Core.throwError ex
+| Except.error ex => throwError ex
 | Except.ok p     => do
   let leading    := p.1;
   let parser     := p.2;
   let tokens     := parser.info.collectTokens [];
   tokens.forM fun token => do {
-    env ← Core.getEnv;
+    env ← getEnv;
     match addToken env token with
-      | Except.ok env    => Core.setEnv env
-      | Except.error msg => Core.throwError ("invalid parser '" ++ toString declName ++ "', " ++ msg)
+      | Except.ok env    => setEnv env
+      | Except.error msg => throwError ("invalid parser '" ++ toString declName ++ "', " ++ msg)
   };
   let kinds := parser.info.collectKinds {};
-  kinds.forM fun kind _ => Core.modifyEnv fun env => addSyntaxNodeKind env kind;
+  kinds.forM fun kind _ => modifyEnv fun env => addSyntaxNodeKind env kind;
   match addParser categories catName declName leading parser with
-  | Except.ok _     => Core.modifyEnv fun env => parserExtension.addEntry env $ ParserExtensionEntry.parser catName declName leading parser
-  | Except.error ex => Core.throwError ex;
+  | Except.ok _     => modifyEnv fun env => parserExtension.addEntry env $ ParserExtensionEntry.parser catName declName leading parser
+  | Except.error ex => throwError ex;
   runParserAttributeHooks catName declName /- builtin -/ false
 
 def mkParserAttributeImpl (attrName : Name) (catName : Name) : AttributeImpl :=
diff --git a/src/Lean/ParserCompiler/Attribute.lean b/src/Lean/ParserCompiler/Attribute.lean
index bbb10cbb58..0fa91659db 100644
--- a/src/Lean/ParserCompiler/Attribute.lean
+++ b/src/Lean/ParserCompiler/Attribute.lean
@@ -28,12 +28,12 @@ let attrImpl : AttributeImpl := {
   name  := name,
   descr := descr,
   add   := fun decl args _ => do
-    env ← Core.getEnv;
+    env ← getEnv;
     match attrParamSyntaxToIdentifier args with
     | some parserDeclName => do
-      _ ← Core.getConstInfo parserDeclName;
-      Core.setEnv $ ext.addEntry env (parserDeclName, decl)
-    | none            => Core.throwError $ "invalid [" ++ name ++ "] argument, expected identifier"
+      _ ← getConstInfo parserDeclName;
+      setEnv $ ext.addEntry env (parserDeclName, decl)
+    | none            => throwError $ "invalid [" ++ name ++ "] argument, expected identifier"
 };
 registerBuiltinAttribute attrImpl;
 pure { attr := attrImpl, ext := ext }
diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean
index f6a53acf05..32c8e38e23 100644
--- a/src/Lean/PrettyPrinter/Formatter.lean
+++ b/src/Lean/PrettyPrinter/Formatter.lean
@@ -130,15 +130,6 @@ fold (Array.foldl (fun acc f => f ++ acc) Format.nil) x
 def concatArgs (x : FormatterM Unit) : FormatterM Unit :=
 concat (visitArgs x)
 
-@[inline] def liftCoreM {α} (x : CoreM α) : FormatterM α :=
-liftM x
-
-def getEnv : FormatterM Environment :=
-liftCoreM Core.getEnv
-
-def throwError {α} (msg : MessageData) : FormatterM α :=
-liftCoreM $ Core.throwError msg
-
 /-
 /--
   Call an appropriate `[formatter]` depending on the `Parser` `Expr` `p`. After the call, the traverser position
@@ -418,7 +409,7 @@ catchInternalId backtrackExceptionId
   (do
     (_, st) ← (formatter { table := table }).run { stxTrav := Syntax.Traverser.fromSyntax stx };
     pure $ st.stack.get! 0)
-  (fun _ => Core.throwError "format: uncaught backtrack exception")
+  (fun _ => throwError "format: uncaught backtrack exception")
 
 def formatTerm := format $ categoryParser.formatter `term
 def formatCommand := format $ categoryParser.formatter `command
diff --git a/src/Lean/PrettyPrinter/Parenthesizer.lean b/src/Lean/PrettyPrinter/Parenthesizer.lean
index 2073970d8d..aacb0cc381 100644
--- a/src/Lean/PrettyPrinter/Parenthesizer.lean
+++ b/src/Lean/PrettyPrinter/Parenthesizer.lean
@@ -255,11 +255,8 @@ arbitrary _
 @[inline] def liftCoreM {α} (x : CoreM α) : ParenthesizerM α :=
 liftM x
 
-def getEnv : ParenthesizerM Environment :=
-liftCoreM Core.getEnv
-
 def throwError {α} (msg : MessageData) : ParenthesizerM α :=
-liftCoreM $ Core.throwError msg
+liftCoreM $ throwError msg
 
 def parenthesizerForKind (k : SyntaxNodeKind) : Parenthesizer := do
 env ← getEnv;
@@ -452,7 +449,7 @@ catchInternalId backtrackExceptionId
   (do
     (_, st) ← (parenthesizer {}).run { stxTrav := Syntax.Traverser.fromSyntax stx };
     pure st.stxTrav.cur)
-  (fun _ => Core.throwError "parenthesize: uncaught backtrack exception")
+  (fun _ => throwError "parenthesize: uncaught backtrack exception")
 
 def parenthesizeTerm := parenthesize $ categoryParser.parenthesizer `term 0
 def parenthesizeCommand := parenthesize $ categoryParser.parenthesizer `command 0
diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean
index 4a9189f097..dc79baae36 100644
--- a/tests/lean/run/Reparen.lean
+++ b/tests/lean/run/Reparen.lean
@@ -42,7 +42,7 @@ stx' ← PrettyPrinter.parenthesizeTerm stx';
 f ← PrettyPrinter.formatTerm stx';
 IO.println f;
 when (stx != stx') $
-  Core.throwError "reparenthesization failed"
+  throwError "reparenthesization failed"
 
 new_frontend
 
diff --git a/tests/lean/run/eval_unboxed_const.lean b/tests/lean/run/eval_unboxed_const.lean
index 89535e2494..8f44cac2e8 100644
--- a/tests/lean/run/eval_unboxed_const.lean
+++ b/tests/lean/run/eval_unboxed_const.lean
@@ -4,7 +4,7 @@ open Lean
 def c1 : Bool := true
 
 unsafe def tst1 : CoreM Unit := do
-env ← Core.getEnv;
+env ← getEnv;
 let v := env.evalConst Bool `c1;
 IO.println v
 
@@ -13,7 +13,7 @@ IO.println v
 def c2 : Bool := false
 
 unsafe def tst2 : CoreM Unit := do
-env ← Core.getEnv;
+env ← getEnv;
 let v := env.evalConst Bool `c2;
 IO.println v
 
diff --git a/tests/lean/run/evalconst.lean b/tests/lean/run/evalconst.lean
index ec77eac088..1dcefe7dd8 100644
--- a/tests/lean/run/evalconst.lean
+++ b/tests/lean/run/evalconst.lean
@@ -4,7 +4,7 @@ open Lean
 def x := 10
 
 unsafe def tst : CoreM Unit := do
-env ← Core.getEnv;
+env ← getEnv;
 IO.println $ env.evalConst Nat `x;
 pure ()
 
@@ -13,7 +13,7 @@ pure ()
 def f (x : Nat) := x + 1
 
 unsafe def tst2 : CoreM Unit := do
-env ← Core.getEnv;
+env ← getEnv;
 f ← liftIO $ IO.ofExcept $ env.evalConst (Nat → Nat) `f;
 IO.println $ (f 10);
 pure ()
diff --git a/tests/lean/run/frontend1.lean b/tests/lean/run/frontend1.lean
index 5ef4dadec4..99c2c80b7c 100644
--- a/tests/lean/run/frontend1.lean
+++ b/tests/lean/run/frontend1.lean
@@ -3,12 +3,12 @@ open Lean
 open Lean.Elab
 
 def run (input : String) (failIff : Bool := true) : CoreM Unit :=
-do env  ← Core.getEnv;
-   opts ← Core.getOptions;
+do env  ← getEnv;
+   opts ← getOptions;
    (env, messages) ← liftIO $ process input env opts;
    messages.forM $ fun msg => IO.println msg;
-   when (failIff && messages.hasErrors) $ Core.throwError "errors have been found";
-   when (!failIff && !messages.hasErrors) $ Core.throwError "there are no errors";
+   when (failIff && messages.hasErrors) $ throwError "errors have been found";
+   when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
    pure ()
 
 def fail (input : String) : CoreM Unit :=
diff --git a/tests/lean/run/kernel1.lean b/tests/lean/run/kernel1.lean
index e7f5c151e8..f7c91ae632 100644
--- a/tests/lean/run/kernel1.lean
+++ b/tests/lean/run/kernel1.lean
@@ -3,7 +3,7 @@ import Lean
 open Lean
 
 def checkDefEq (a b : Name) : CoreM Unit := do
-env ← Core.getEnv;
+env ← getEnv;
 let a := mkConst a;
 let b := mkConst b;
 let r := Kernel.isDefEq env {} a b;
diff --git a/tests/lean/run/kernel2.lean b/tests/lean/run/kernel2.lean
index 6b081fc7e2..b36891faed 100644
--- a/tests/lean/run/kernel2.lean
+++ b/tests/lean/run/kernel2.lean
@@ -2,14 +2,14 @@ import Lean
 open Lean
 
 def checkDefEq (a b : Name) : CoreM Unit := do
-env ← Core.getEnv;
+env ← getEnv;
 let a := mkConst a;
 let b := mkConst b;
 let r := Kernel.isDefEq env {} a b;
 IO.println (toString a ++ " =?= " ++ toString b ++ " := " ++ toString r)
 
 def whnf (a : Name) : CoreM Unit := do
-env ← Core.getEnv;
+env ← getEnv;
 let a := mkConst a;
 let r := Kernel.whnf env {} a;
 IO.println (toString a ++ " ==> " ++ toString r)
diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean
index 83b7bbb6b1..c00bd5bdaa 100644
--- a/tests/lean/run/structure.lean
+++ b/tests/lean/run/structure.lean
@@ -14,7 +14,7 @@ structure S4 extends S2, S3 :=
 (s : Nat)
 
 def check (b : Bool) : CoreM Unit :=
-unless b $ Core.throwError "check failed"
+unless b $ throwError "check failed"
 
 class S5 :=
 (x y : Nat)
@@ -23,7 +23,7 @@ inductive D
 | mk (x y z : Nat) : D
 
 def tst : CoreM Unit :=
-do env ← Core.getEnv;
+do env ← getEnv;
    IO.println (getStructureFields env `Lean.Environment);
    check $ getStructureFields env `S4 == #[`toS2, `toS3, `s];
    check $ getStructureFields env `S1 == #[`x, `y];
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index 6be1e1a4e1..8e8f8e7597 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -3,12 +3,12 @@ open Lean
 open Lean.Elab
 
 def run (input : String) (failIff : Bool := true) : CoreM Unit :=
-do env  ← Core.getEnv;
-   opts ← Core.getOptions;
+do env  ← getEnv;
+   opts ← getOptions;
    (env, messages) ← liftIO $ process input env opts;
    messages.toList.forM $ fun msg => liftIO $ IO.println msg;
-   when (failIff && messages.hasErrors) $ Core.throwError "errors have been found";
-   when (!failIff && !messages.hasErrors) $ Core.throwError "there are no errors";
+   when (failIff && messages.hasErrors) $ throwError "errors have been found";
+   when (!failIff && !messages.hasErrors) $ throwError "there are no errors";
    pure ()
 
 open Lean.Parser
diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean
index acd8df0b6f..0097e8d634 100644
--- a/tests/lean/run/toExpr.lean
+++ b/tests/lean/run/toExpr.lean
@@ -3,7 +3,7 @@ import Lean
 open Lean
 
 unsafe def test {α : Type} [HasToString α] [ToExpr α] [HasBeq α] (a : α) : CoreM Unit := do
-env ← Core.getEnv;
+env ← getEnv;
 let auxName := `_toExpr._test;
 let decl := Declaration.defnDecl {
   name     := auxName,
@@ -15,14 +15,14 @@ let decl := Declaration.defnDecl {
 };
 IO.println (toExpr a);
 match env.addAndCompile {} decl with
-| Except.error _ => Core.throwError "addDecl failed"
+| Except.error _ => throwError "addDecl failed"
 | Except.ok env  => do
   match env.evalConst α auxName with
-  | Except.error ex => Core.throwError ex
+  | Except.error ex => throwError ex
   | Except.ok b => do
     IO.println b;
     unless (a == b) $
-      Core.throwError "toExpr failed";
+      throwError "toExpr failed";
     pure ()
 
 #eval test #[(1, 2), (3, 4)]