diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean
index 630546efca..274725317c 100644
--- a/src/Lean/Attributes.lean
+++ b/src/Lean/Attributes.lean
@@ -5,6 +5,7 @@ Authors: Leonardo de Moura
 -/
 import Lean.Scopes
 import Lean.Syntax
+import Lean.CoreM
 
 namespace Lean
 
@@ -25,7 +26,7 @@ instance AttributeApplicationTime.hasBeq : HasBeq AttributeApplicationTime := 
 structure AttributeImpl :=
 (name : Name)
 (descr : String)
-(add (env : Environment) (decl : Name) (args : Syntax) (persistent : Bool) : IO Environment)
+(add (decl : Name) (args : Syntax) (persistent : Bool) : CoreM Unit)
 /-
 (addScoped (env : Environment) (decl : Name) (args : Syntax) : IO Environment
            := throw (IO.userError ("attribute '" ++ toString name ++ "' does not support scopes")))
@@ -38,7 +39,7 @@ structure AttributeImpl :=
 (applicationTime := AttributeApplicationTime.afterTypeChecking)
 
 instance AttributeImpl.inhabited : Inhabited AttributeImpl :=
-⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure env }⟩
+⟨{ name := arbitrary _, descr := arbitrary _, add := fun env _ _ _ => pure () }⟩
 
 open Std (PersistentHashMap)
 
@@ -190,7 +191,8 @@ namespace Environment
 @[export lean_add_attribute]
 def addAttribute (env : Environment) (decl : Name) (attrName : Name) (args : Syntax := Syntax.missing) (persistent := true) : IO Environment := do
 attr ← IO.ofExcept $ getAttributeImpl env attrName;
-attr.add env decl args persistent
+(env, _) ← Core.runCore (attr.add decl args persistent) env;
+pure env
 
 /-
 /- Add a scoped attribute `attr` to declaration `decl` with arguments `args` and scope `decl.getPrefix`.
@@ -262,7 +264,7 @@ structure TagAttribute :=
 (attr : AttributeImpl)
 (ext  : PersistentEnvExtension Name Name NameSet)
 
-def registerTagAttribute (name : Name) (descr : String) (validate : Environment → Name → Except String Unit := fun _ _ => Except.ok ()) : IO TagAttribute := do
+def registerTagAttribute (name : Name) (descr : String) (validate : Name → CoreM Unit := fun _ => pure ()) : IO TagAttribute := do
 ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtension {
   name            := name,
   mkInitial       := pure {},
@@ -276,14 +278,14 @@ ext : PersistentEnvExtension Name Name NameSet ← registerPersistentEnvExtensio
 let attrImpl : AttributeImpl := {
   name  := name,
   descr := descr,
-  add   := fun env decl args persistent => do
-    when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', unexpected argument"));
-    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
+  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;
     unless (env.getModuleIdxFor? decl).isNone $
-      throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
-    match validate env decl with
-    | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-    | _                => pure $ ext.addEntry env decl
+      Core.throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
+    validate decl;
+    Core.setEnv $ ext.addEntry env decl
 };
 registerBuiltinAttribute attrImpl;
 pure { attr := attrImpl, ext := ext }
@@ -310,8 +312,8 @@ structure ParametricAttribute (α : Type) :=
 (ext  : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
 
 def registerParametricAttribute {α : Type} [Inhabited α] (name : Name) (descr : String)
-    (getParam : Environment → Name → Syntax → Except String α)
-    (afterSet : Environment → Name → α → Except String Environment := fun env _ _ => Except.ok env)
+    (getParam : Name → Syntax → CoreM α)
+    (afterSet : Name → α → CoreM Unit := fun env _ _ => pure ())
     (appTime := AttributeApplicationTime.afterTypeChecking)
     : IO (ParametricAttribute α) := do
 ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
@@ -328,17 +330,15 @@ let attrImpl : AttributeImpl := {
   name  := name,
   descr := descr,
   applicationTime := appTime,
-  add   := fun env decl args persistent => do
-    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
+  add   := fun decl args persistent => do
+    unless persistent $ Core.throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
+    env ← Core.getEnv;
     unless (env.getModuleIdxFor? decl).isNone $
-      throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
-    match getParam env decl args with
-    | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-    | Except.ok val    => do
-      let env := ext.addEntry env (decl, val);
-      match afterSet env decl val with
-      | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-      | Except.ok env    => pure env
+      Core.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)
 };
 registerBuiltinAttribute attrImpl;
 pure { attr := attrImpl, ext := ext }
@@ -373,7 +373,9 @@ structure EnumAttributes (α : Type) :=
 (attrs : List AttributeImpl)
 (ext   : PersistentEnvExtension (Name × α) (Name × α) (NameMap α))
 
-def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α)) (validate : Environment → Name → α → Except String Unit := fun _ _ _ => Except.ok ()) (applicationTime := AttributeApplicationTime.afterTypeChecking) : IO (EnumAttributes α) := do
+def registerEnumAttributes {α : Type} [Inhabited α] (extName : Name) (attrDescrs : List (Name × String × α))
+    (validate : Name → α → CoreM Unit := fun _ _ => pure ())
+    (applicationTime := AttributeApplicationTime.afterTypeChecking) : IO (EnumAttributes α) := do
 ext : PersistentEnvExtension (Name × α) (Name × α) (NameMap α) ← registerPersistentEnvExtension {
   name            := extName,
   mkInitial       := pure {},
@@ -388,13 +390,13 @@ let attrs := attrDescrs.map $ fun ⟨name, descr, val⟩ => {
   name            := name,
   descr           := descr,
   applicationTime := applicationTime,
-  add             := (fun env decl args persistent => do
-    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString name ++ "', must be persistent"));
+  add             := (fun decl args persistent => do
+    unless persistent $ Core.throwError ("invalid attribute '" ++ toString name ++ "', must be persistent");
+    env ← Core.getEnv;
     unless (env.getModuleIdxFor? decl).isNone $
-      throw (IO.userError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module"));
-    match validate env decl val with
-    | Except.error msg => throw (IO.userError ("invalid attribute '" ++ toString name ++ "', " ++ msg))
-    | _                => pure $ ext.addEntry env (decl, val))
+      Core.throwError ("invalid attribute '" ++ toString name ++ "', declaration is in an imported module");
+    validate decl val;
+    Core.setEnv $ ext.addEntry env (decl, val))
   : AttributeImpl
 };
 attrs.forM registerBuiltinAttribute;
diff --git a/src/Lean/Class.lean b/src/Lean/Class.lean
index 9704703220..28ad5746a3 100644
--- a/src/Lean/Class.lean
+++ b/src/Lean/Class.lean
@@ -139,10 +139,12 @@ partial def getClassName (env : Environment) : Expr → Option Name
 registerBuiltinAttribute {
   name  := `class,
   descr := "type class",
-  add   := fun env decl args persistent => do
-    when args.hasArgs $ throw (IO.userError ("invalid attribute 'class', unexpected argument"));
-    unless persistent $ throw (IO.userError ("invalid attribute 'class', must be persistent"));
-    IO.ofExcept (addClass env decl)
+  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
 }
 
 -- TODO: delete
diff --git a/src/Lean/Compiler/ExportAttr.lean b/src/Lean/Compiler/ExportAttr.lean
index 88c350dd19..237797a6d7 100644
--- a/src/Lean/Compiler/ExportAttr.lean
+++ b/src/Lean/Compiler/ExportAttr.lean
@@ -17,12 +17,12 @@ private def isValidCppName : Name → Bool
 | _                           => false
 
 def mkExportAttr : IO (ParametricAttribute Name) :=
-registerParametricAttribute `export "name to be used by code generators" $ fun _ _ stx =>
+registerParametricAttribute `export "name to be used by code generators" $ fun _ stx =>
   match attrParamSyntaxToIdentifier stx with
   | some exportName =>
-    if isValidCppName exportName then Except.ok exportName
-    else Except.error "invalid 'export' function name, is not a valid C++ identifier"
-  | _ => Except.error "unexpected kind of argument"
+    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"
 
 @[init mkExportAttr]
 constant exportAttr : ParametricAttribute Name := arbitrary _
diff --git a/src/Lean/Compiler/ExternAttr.lean b/src/Lean/Compiler/ExternAttr.lean
index 0f17ef4e37..d1594f227c 100644
--- a/src/Lean/Compiler/ExternAttr.lean
+++ b/src/Lean/Compiler/ExternAttr.lean
@@ -80,12 +80,14 @@ constant addExtern (env : Environment) (n : Name) : ExceptT String Id Environmen
 
 def mkExternAttr : IO (ParametricAttribute ExternAttrData) :=
 registerParametricAttribute `extern "builtin and foreign functions"
-  (fun _ _ => syntaxToExternAttrData)
-  (fun env declName _ =>
-    if env.isProjectionFn declName || env.isConstructor declName then
-      addExtern env declName
+  (fun _ stx => Core.ofExcept $ syntaxToExternAttrData stx)
+  (fun declName _ => do
+    env ← Core.getEnv;
+    if env.isProjectionFn declName || env.isConstructor declName then do
+      env ← Core.ofExcept $ addExtern env declName;
+      Core.setEnv env
     else
-      pure env)
+      pure ())
 
 @[init mkExternAttr]
 constant externAttr : ParametricAttribute ExternAttrData := arbitrary _
diff --git a/src/Lean/Compiler/IR/UnboxResult.lean b/src/Lean/Compiler/IR/UnboxResult.lean
index 39951f1e3d..483b5a862e 100644
--- a/src/Lean/Compiler/IR/UnboxResult.lean
+++ b/src/Lean/Compiler/IR/UnboxResult.lean
@@ -11,14 +11,13 @@ namespace IR
 namespace UnboxResult
 
 def mkUnboxAttr : IO TagAttribute :=
-registerTagAttribute `unbox "compiler tries to unbox result values if their types are tagged with `[unbox]`" $ fun env declName =>
-  match env.find? declName with
-  | none => Except.error "unknown declaration"
-  | some cinfo => match cinfo with
-    | ConstantInfo.inductInfo v =>
-      if v.isRec then Except.error "recursive inductive datatypes are not supported"
-      else Except.ok ()
-    | _ => Except.error "constant must be an inductive type"
+registerTagAttribute `unbox "compiler tries to unbox result values if their types are tagged with `[unbox]`" $ fun declName => do
+  cinfo ← Core.getConstInfo declName;
+  match cinfo with
+  | ConstantInfo.inductInfo v =>
+    if v.isRec then Core.throwError "recursive inductive datatypes are not supported"
+    else pure ()
+  | _ => Core.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 f5fb6e17a4..a30ab9e023 100644
--- a/src/Lean/Compiler/ImplementedByAttr.lean
+++ b/src/Lean/Compiler/ImplementedByAttr.lean
@@ -9,18 +9,14 @@ namespace Lean
 namespace Compiler
 
 def mkImplementedByAttr : IO (ParametricAttribute Name) :=
-registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) function that implements opaque constant" $ fun env declName stx =>
-  match env.find? declName with
-  | none => Except.error "unknown declaration"
-  | some decl =>
-    match attrParamSyntaxToIdentifier stx with
-    | some fnName =>
-      match env.find? fnName with
-      | none => Except.error ("unknown function '" ++ toString fnName ++ "'")
-      | some fnDecl =>
-        if decl.type == fnDecl.type then Except.ok fnName
-        else Except.error ("invalid function '" ++ toString fnName ++ "' type mismatch")
-    | _ => Except.error "expected identifier"
+registerParametricAttribute `implementedBy "name of the Lean (probably unsafe) function that implements opaque constant" fun declName stx => do
+  decl ← Core.getConstInfo declName;
+  match attrParamSyntaxToIdentifier stx with
+  | some fnName => do
+    fnDecl ← Core.getConstInfo fnName;
+    if decl.type == fnDecl.type then pure fnName
+    else Core.throwError ("invalid function '" ++ fnName ++ "' type mismatch")
+  | _ => Core.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 fc82818dec..939a279337 100644
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -22,25 +22,21 @@ match getIOTypeArg type with
 | _ => false
 
 def mkInitAttr : IO (ParametricAttribute Name) :=
-registerParametricAttribute `init "initialization procedure for global references" $ fun env declName stx =>
-  match env.find? declName with
-  | none => Except.error "unknown declaration"
-  | some decl =>
-    match attrParamSyntaxToIdentifier stx with
-    | some initFnName =>
-      match env.find? initFnName with
-      | none => Except.error ("unknown initialization function '" ++ toString initFnName ++ "'")
-      | some initDecl =>
-        match getIOTypeArg initDecl.type with
-        | none => Except.error ("initialization function '" ++ toString initFnName ++ "' must have type of the form `IO <type>`")
-        | some initTypeArg =>
-          if decl.type == initTypeArg then Except.ok initFnName
-          else Except.error ("initialization function '" ++ toString initFnName ++ "' type mismatch")
-    | _ => match stx with
-      | Syntax.missing =>
-        if isIOUnit decl.type then Except.ok Name.anonymous
-        else Except.error "initialization function must have type `IO Unit`"
-      | _ => Except.error "unexpected kind of argument"
+registerParametricAttribute `init "initialization procedure for global references" $ fun declName stx => do
+  decl ← Core.getConstInfo declName;
+  match attrParamSyntaxToIdentifier stx with
+  | some initFnName => do
+    initDecl ← Core.getConstInfo initFnName;
+    match getIOTypeArg initDecl.type with
+    | none => Core.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")
+  | _ => 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"
 
 @[init mkInitAttr]
 constant initAttr : ParametricAttribute Name := arbitrary _
diff --git a/src/Lean/Compiler/InlineAttrs.lean b/src/Lean/Compiler/InlineAttrs.lean
index d0f57d6f48..1975249874 100644
--- a/src/Lean/Compiler/InlineAttrs.lean
+++ b/src/Lean/Compiler/InlineAttrs.lean
@@ -33,7 +33,9 @@ registerEnumAttributes `inlineAttrs
    (`inlineIfReduce, "mark definition to be inlined when resultant term after reduction is not a `cases_on` application", InlineAttributeKind.inlineIfReduce),
    (`noinline, "mark definition to never be inlined", InlineAttributeKind.noinline),
    (`macroInline, "mark definition to always be inlined before ANF conversion", InlineAttributeKind.macroInline)]
-  (fun env declName _ => checkIsDefinition env declName)
+  (fun declName _ => do
+    env ← Core.getEnv;
+    Core.ofExcept $ checkIsDefinition env declName)
 
 @[init mkInlineAttrs]
 constant inlineAttrs : EnumAttributes InlineAttributeKind := arbitrary _
diff --git a/src/Lean/Compiler/Specialize.lean b/src/Lean/Compiler/Specialize.lean
index a67cbcdf55..e5b4a9fc09 100644
--- a/src/Lean/Compiler/Specialize.lean
+++ b/src/Lean/Compiler/Specialize.lean
@@ -38,7 +38,7 @@ registerEnumAttributes `specializeAttrs
      In the new equation compiler we should pass all attributes and allow it to apply them to auxiliary definitions.
      In the current implementation, we workaround this issue by using functions such as `hasSpecializeAttrAux`.
    -/
-  (fun env declName _ => Except.ok ())
+  (fun declName _ => pure ())
   AttributeApplicationTime.beforeElaboration
 
 @[init mkSpecializeAttrs]
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 52ef87be81..8d58bd9201 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -54,6 +54,11 @@ def throwError {α} (msg : MessageData) : CoreM α := do
 ctx ← read;
 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
@@ -70,6 +75,9 @@ 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 {ε} : ECoreM ε Options :=  do
 ctx ← read; pure ctx.options
 
diff --git a/src/Lean/Elab/DeclModifiers.lean b/src/Lean/Elab/DeclModifiers.lean
index a51b0796aa..c36b37110e 100644
--- a/src/Lean/Elab/DeclModifiers.lean
+++ b/src/Lean/Elab/DeclModifiers.lean
@@ -159,7 +159,7 @@ attrs.forM $ fun attr => do
  | Except.ok attrImpl  =>
    when (attrImpl.applicationTime == applicationTime) $ do
      env ← getEnv;
-     env ← liftIO $ attrImpl.add env declName attr.args true;
+     (env, _) ← liftIO $ Core.runCore (attrImpl.add declName attr.args true) env; -- TODO: revise after MetaM refactoring
      setEnv env
 
 end Command
diff --git a/src/Lean/KeyedDeclsAttribute.lean b/src/Lean/KeyedDeclsAttribute.lean
index d6d2d38bfa..a5abe21677 100644
--- a/src/Lean/KeyedDeclsAttribute.lean
+++ b/src/Lean/KeyedDeclsAttribute.lean
@@ -127,27 +127,29 @@ ext : Extension γ ← registerPersistentEnvExtension {
 registerBuiltinAttribute {
   name  := df.builtinName,
   descr := "(builtin) " ++ df.descr,
-  add   := fun env declName arg persistent => do {
-    unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString df.builtinName ++ "', must be persistent"));
-    key ← IO.ofExcept $ df.evalKey true env arg;
-    match env.find? declName with
-    | none  => throw $ IO.userError "unknown declaration"
-    | some decl =>
-      match decl.type with
-      | Expr.const c _ _ =>
-        if c != df.valueTypeName then throw (IO.userError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected"))
-        else declareBuiltin df attrDeclName env key declName
-      | _ => throw (IO.userError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected"))
+  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;
+    match decl.type with
+    | Expr.const c _ _ =>
+      if c != df.valueTypeName then Core.throwError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected")
+      else do
+        env ← liftM $ declareBuiltin df attrDeclName env key declName;
+        Core.setEnv env
+    | _ => Core.throwError ("unexpected type at '" ++ toString declName ++ "', `" ++ toString df.valueTypeName ++ "` expected")
   },
   applicationTime := AttributeApplicationTime.afterCompilation
 };
 registerBuiltinAttribute {
   name            := df.name,
   descr           := df.descr,
-  add             := fun env constName arg persistent => do
-    key ← IO.ofExcept $ df.evalKey false env arg;
-    val ← IO.ofExcept $ env.evalConstCheck γ df.valueTypeName constName;
-    pure $ ext.addEntry env { key := key, decl := constName, value := val },
+  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 },
   applicationTime := AttributeApplicationTime.afterCompilation
 };
 pure { tableRef := tableRef, ext := ext }
diff --git a/src/Lean/Meta/Instances.lean b/src/Lean/Meta/Instances.lean
index cc09ce7bd1..267851f6af 100644
--- a/src/Lean/Meta/Instances.lean
+++ b/src/Lean/Meta/Instances.lean
@@ -46,11 +46,13 @@ match env.find? constName with
 registerBuiltinAttribute {
   name  := `instance,
   descr := "type class instance",
-  add   := fun env declName args persistent => do
-    when args.hasArgs $ throw (IO.userError ("invalid attribute 'instance', unexpected argument"));
-    unless persistent $ throw (IO.userError ("invalid attribute 'instance', must be persistent"));
-    env ← IO.ofExcept (addGlobalInstanceOld env declName); -- TODO: delete
-    addGlobalInstance env declName
+  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
+    env ← liftM $ addGlobalInstance env declName;
+    Core.setEnv env
 }
 
 end Meta
diff --git a/src/Lean/Meta/RecursorInfo.lean b/src/Lean/Meta/RecursorInfo.lean
index 106ac685d3..5198751f83 100644
--- a/src/Lean/Meta/RecursorInfo.lean
+++ b/src/Lean/Meta/RecursorInfo.lean
@@ -290,11 +290,13 @@ match cinfo with
 
 def mkRecursorAttr : IO (ParametricAttribute Nat) :=
 registerParametricAttribute `recursor "user defined recursor, numerical parameter specifies position of the major premise"
-  (fun _ _ => syntaxToMajorPos)
-  (fun env declName majorPos =>
-    match Meta.run env (mkRecursorInfoCore declName (some majorPos)) with
-    | Except.ok _     => pure env
-    | Except.error ex => Except.error $ toString ex)
+  (fun _ stx => Core.ofExcept $ syntaxToMajorPos stx)
+  (fun declName majorPos => do
+    -- TODO: new code after CoreM refactoring
+    -- Meta.run $ mkRecursorInfoCore declName (some majorPos)
+    env ← Core.getEnv;
+    (info, env) ← liftM $ IO.runMeta (mkRecursorInfoCore declName (some majorPos)) env;
+    Core.setEnv env)
 
 @[init mkRecursorAttr] constant recursorAttribute : ParametricAttribute Nat := arbitrary _
 
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index ab8f93cb8b..44b34596da 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -225,7 +225,7 @@ mkParserOfConstantAux env categories constName (compileParserDescr env categorie
 
 structure ParserAttributeHook :=
 /- Called after a parser attribute is applied to a declaration. -/
-(postAdd : forall (catName : Name) (env : Environment) (declName : Name) (builtin : Bool), IO Environment)
+(postAdd : forall (catName : Name) (env : Environment) (declName : Name) (builtin : Bool), IO Environment) -- TODO: use CoreM?
 
 def mkParserAttributeHooks : IO (IO.Ref (List ParserAttributeHook)) := IO.mkRef {}
 @[init mkParserAttributeHooks] constant parserAttributeHooks : IO.Ref (List ParserAttributeHook) := arbitrary _
@@ -357,28 +357,31 @@ match env.addAndCompile {} decl with
 | Except.error _ => throw (IO.userError ("failed to emit registration code for builtin parser '" ++ toString declName ++ "'"))
 | Except.ok env  => IO.ofExcept (setInitAttr env name)
 
-def declareLeadingBuiltinParser (env : Environment) (catName : Name) (declName : Name) : IO Environment :=
+def declareLeadingBuiltinParser (env : Environment) (catName : Name) (declName : Name) : IO Environment := -- TODO: use CoreM?
 declareBuiltinParser env `Lean.Parser.addBuiltinLeadingParser catName declName
 
-def declareTrailingBuiltinParser (env : Environment) (catName : Name) (declName : Name) : IO Environment :=
+def declareTrailingBuiltinParser (env : Environment) (catName : Name) (declName : Name) : IO Environment := -- TODO: use CoreM?
 declareBuiltinParser env `Lean.Parser.addBuiltinTrailingParser catName declName
 
 private def BuiltinParserAttribute.add (attrName : Name) (catName : Name)
-    (env : Environment) (declName : Name) (args : Syntax) (persistent : Bool) : IO Environment := do
-when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
-unless persistent $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', must be persistent"));
-env ← match env.find? declName with
-| none  => throw $ IO.userError "unknown declaration"
-| some decl =>
-  match decl.type with
- | Expr.const `Lean.Parser.TrailingParser _ _ =>
-   declareTrailingBuiltinParser env catName declName
- | Expr.const `Lean.Parser.Parser _ _ =>
-   declareLeadingBuiltinParser env catName declName
- | _ =>
-   throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"));
+    (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;
+match decl.type with
+| Expr.const `Lean.Parser.TrailingParser _ _ => do
+  env ← liftM $ declareTrailingBuiltinParser env catName declName;
+  Core.setEnv env
+| Expr.const `Lean.Parser.Parser _ _ => do
+  env ← liftM $ declareLeadingBuiltinParser env catName declName;
+  Core.setEnv env
+| _ => Core.throwError ("unexpected parser type at '" ++ declName ++ "' (`Parser` or `TrailingParser` expected");
 hooks ← parserAttributeHooks.get;
-hooks.foldlM (fun env hook => hook.postAdd catName env declName /- builtin -/ true) env
+hooks.forM fun hook => do
+  env ← Core.getEnv;
+  env ← liftM $ hook.postAdd catName env declName /- builtin -/ true;
+  Core.setEnv env
 
 /-
 The parsing tables for builtin parsers are "stored" in the extracted source code.
@@ -392,28 +395,32 @@ registerBuiltinAttribute {
  applicationTime := AttributeApplicationTime.afterCompilation
 }
 
-private def ParserAttribute.add (attrName : Name) (catName : Name) (env : Environment) (declName : Name) (args : Syntax) (persistent : Bool) : IO Environment := do
-when args.hasArgs $ throw (IO.userError ("invalid attribute '" ++ toString attrName ++ "', unexpected argument"));
+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;
 let categories := (parserExtension.getState env).categories;
 match mkParserOfConstant env categories declName with
-| Except.error ex => throw (IO.userError ex)
+| Except.error ex => Core.throwError ex
 | Except.ok p     => do
   let leading    := p.1;
   let parser     := p.2;
   let tokens     := parser.info.collectTokens [];
-  env ← tokens.foldlM
-    (fun env token =>
-      match addToken env token with
-      | Except.ok env    => pure env
-      | Except.error msg => throw (IO.userError ("invalid parser '" ++ toString declName ++ "', " ++ msg)))
-    env;
+  tokens.forM fun token => do {
+    env ← Core.getEnv;
+    match addToken env token with
+      | Except.ok env    => Core.setEnv env
+      | Except.error msg => Core.throwError ("invalid parser '" ++ toString declName ++ "', " ++ msg)
+  };
   let kinds := parser.info.collectKinds {};
-  let env := kinds.foldl (fun env kind _ => addSyntaxNodeKind env kind) env;
-  env ← match addParser categories catName declName leading parser with
-  | Except.ok _     => pure $ parserExtension.addEntry env $ ParserExtensionEntry.parser catName declName leading parser
-  | Except.error ex => throw (IO.userError ex);
+  kinds.forM fun kind _ => Core.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;
   hooks ← parserAttributeHooks.get;
-  hooks.foldlM (fun env hook => hook.postAdd catName env declName /- builtin -/ false) env
+  hooks.forM fun hook => do
+    env ← Core.getEnv;
+    env ← liftM $ hook.postAdd catName env declName /- builtin -/ false;
+    Core.setEnv env
 
 def mkParserAttributeImpl (attrName : Name) (catName : Name) : AttributeImpl :=
 { name            := attrName,
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index f509f09a9f..38cdc377c6 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -30,11 +30,13 @@ ext : SimplePersistentEnvExtension (Name × Name) (NameMap Name) ← registerSim
 let attrImpl : AttributeImpl := {
   name  := name,
   descr := descr,
-  add   := fun env decl args _ => match attrParamSyntaxToIdentifier args with
-    | some parserDecl => match env.find? parserDecl with
-      | some _ => pure $ ext.addEntry env (parserDecl, decl)
-      | none   => throw $ IO.userError $ "invalid [" ++ toString name ++ "] argument, unknown declaration '" ++ toString parserDecl ++ "'"
-    | none            => throw $ IO.userError $ "invalid [" ++ toString name ++ "] argument, expected identifier"
+  add   := fun decl args _ => do
+    env ← Core.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"
 };
 registerBuiltinAttribute attrImpl;
 pure { attr := attrImpl, ext := ext }