diff --git a/src/frontends/lean/decl_attributes.cpp b/src/frontends/lean/decl_attributes.cpp
index f0dae6f380..2f532a05e5 100644
--- a/src/frontends/lean/decl_attributes.cpp
+++ b/src/frontends/lean/decl_attributes.cpp
@@ -303,19 +303,16 @@ environment decl_attributes::apply_all(environment env, io_state const & ios, na
 }
 
 bool decl_attributes::ok_for_inductive_type() const {
-    for (entry const & e : m_entries) {
-        name const & n = e.m_attr->get_name();
-        if (is_system_attribute(n)) {
-            if (n != "class" || e.deleted())
-                return false;
-        }
+    for (new_entry const & e : m_after_tc_entries) {
+        if (e.m_attr != "class" || e.m_deleted)
+            return false;
     }
     return true;
 }
 
 bool decl_attributes::has_class() const {
-    for (entry const & e : m_entries)
-        if (e.m_attr->get_name() == "class" && !e.deleted())
+    for (new_entry const & e : m_after_tc_entries)
+        if (e.m_attr == "class" && !e.m_deleted)
             return true;
     return false;
 }
diff --git a/src/library/class.cpp b/src/library/class.cpp
index 1db7d1aeca..0c4cd37bdd 100644
--- a/src/library/class.cpp
+++ b/src/library/class.cpp
@@ -5,217 +5,25 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
-#include "runtime/sstream.h"
-#include "util/lbool.h"
-#include "util/fresh_name.h"
-#include "util/name_set.h"
-#include "kernel/instantiate.h"
-#include "kernel/for_each_fn.h"
-#include "library/scoped_ext.h"
-#include "library/constants.h"
-#include "library/protected.h"
 #include "library/class.h"
-#include "library/attribute_manager.h"
-#include "library/trace.h"
 
 namespace lean {
-enum class class_entry_kind { Class, Instance };
-struct class_entry {
-    class_entry_kind m_kind;
-    name             m_class;
-    name             m_instance;    // only relevant if m_kind == Instance
-    class_entry():m_kind(class_entry_kind::Class) {}
-    explicit class_entry(name const & c):m_kind(class_entry_kind::Class), m_class(c) {}
-    class_entry(class_entry_kind k, name const & c, name const & i):
-        m_kind(k), m_class(c), m_instance(i) {}
-};
+uint8 is_class_core(object* env, object* n);
+uint8 is_instance_core(object* env, object* n);
+object* get_class_instances_core(object* env, object* n);
+uint8 is_out_param_core(object* e);
+uint8 has_out_params_core(object* env, object* n);
+object* add_instance_core(object* env, object* n);
 
-struct class_state {
-    typedef name_map<names> class_instances;
-    typedef name_set        instance_set;
-
-    class_instances       m_instances;
-    instance_set          m_instance_set;
-    name_set              m_has_out_params;
-
-    bool is_instance(name const & i) const {
-        return m_instance_set.contains(i);
-    }
-
-    names insert(name const & inst, names const & insts) const {
-        if (!insts)
-            return names(inst);
-        else
-            return names(inst, insts);
-    }
-
-    void add_class(environment const & env, name const & c) {
-        auto it = m_instances.find(c);
-        if (!it)
-            m_instances.insert(c, names());
-        expr type = env.get(c).get_type();
-        bool has_out_param = false;
-        while (is_pi(type)) {
-            if (is_class_out_param(binding_domain(type))) {
-                has_out_param = true;
-                break;
-            }
-            type = binding_body(type);
-        }
-        if (has_out_param)
-            m_has_out_params.insert(c);
-    }
-
-    void add_instance(name const & c, name const & i) {
-        auto it = m_instances.find(c);
-        if (!it) {
-            m_instances.insert(c, names(i));
-        } else {
-            auto lst = filter(*it, [&](name const & i1) { return i1 != i; });
-            m_instances.insert(c, names(i, lst));
-        }
-        m_instance_set.insert(i);
-    }
-};
-
-static name * g_class_name = nullptr;
-
-struct class_config {
-    typedef class_state state;
-    typedef class_entry entry;
-    static void add_entry(environment const & env, io_state const &, state & s, entry const & e) {
-        switch (e.m_kind) {
-        case class_entry_kind::Class:
-            s.add_class(env, e.m_class);
-            break;
-        case class_entry_kind::Instance:
-            s.add_instance(e.m_class, e.m_instance);
-            break;
-        }
-    }
-
-    static name const & get_class_name() {
-        return *g_class_name;
-    }
-
-    static const char * get_serialization_key() { return "class"; }
-
-    static void  write_entry(serializer & s, entry const & e) {
-        s << static_cast<char>(e.m_kind);
-        switch (e.m_kind) {
-        case class_entry_kind::Class:
-            s << e.m_class;
-            break;
-        case class_entry_kind::Instance:
-            s << e.m_class << e.m_instance;
-            break;
-        }
-    }
-
-    static entry read_entry(deserializer & d) {
-        entry e; char k;
-        d >> k;
-        e.m_kind = static_cast<class_entry_kind>(k);
-        switch (e.m_kind) {
-        case class_entry_kind::Class:
-            d >> e.m_class;
-            break;
-        case class_entry_kind::Instance:
-            d >> e.m_class >> e.m_instance;
-            break;
-        }
-        return e;
-    }
-};
-
-template class scoped_ext<class_config>;
-typedef scoped_ext<class_config> class_ext;
-
-static void check_class(environment const & env, name const & c_name) {
-    env.get(c_name);
-}
-
-static void check_is_class(environment const & env, name const & c_name) {
-    class_state const & s = class_ext::get_state(env);
-    if (!s.m_instances.contains(c_name))
-        throw exception(sstream() << "'" << c_name << "' is not a class");
-}
-
-name get_class_name(environment const & env, expr const & e) {
-    if (!is_constant(e))
-        throw exception("class expected, expression is not a constant");
-    name const & c_name = const_name(e);
-    check_is_class(env, c_name);
-    return c_name;
-}
-
-environment add_class_core(environment const & env, name const &n, bool persistent) {
-    check_class(env, n);
-    return class_ext::add_entry(env, get_dummy_ios(), class_entry(n), persistent);
-}
-
-bool is_class(environment const & env, name const & c) {
-    class_state const & s = class_ext::get_state(env);
-    return s.m_instances.contains(c);
-}
-
-bool has_class_out_params(environment const & env, name const & c) {
-    class_state const & s = class_ext::get_state(env);
-    return s.m_has_out_params.contains(c);
-}
-
-optional<name> get_class(environment const & env, expr type) {
-    while (is_pi(type)) {
-        type = binding_body(type);
-    }
-    expr f = get_app_fn(type);
-    if (!is_constant(f)) return optional<name>();
-    optional<constant_info> info = env.find(const_name(f));
-    if (!info) return optional<name>();
-    if (info->is_definition()) {
-        expr val = info->get_value();
-        unsigned nargs = get_app_num_args(type);
-        for (unsigned i = 0; i < nargs; i++) {
-            if (!is_lambda(val)) return optional<name>();
-            val = binding_body(val);
-        }
-        return get_class(env, val);
-    } else {
-        class_state const & s = class_ext::get_state(env);
-        if (!s.m_instances.contains(const_name(f))) return optional<name>();
-        return optional<name>(const_name(f));
-    }
-}
-
-environment add_instance_core(environment const & env, name const & n, bool persistent) {
-    constant_info info = env.get(n);
-    expr type = info.get_type();
-    optional<name> c = get_class(env, type);
-    if (!c) throw exception("invalid instance, failed to find its class");
-    environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, *c, n),
-                                               persistent);
-    return new_env;
-}
-
-bool is_instance(environment const & env, name const & i) {
-    class_state const & s = class_ext::get_state(env);
-    return s.is_instance(i);
-}
-
-names get_class_instances(environment const & env, name const & c) {
-    class_state const & s = class_ext::get_state(env);
-    return names(s.m_instances.find(c));
-}
-
-static name * g_class_attr_name    = nullptr;
-static name * g_instance_attr_name = nullptr;
-
-environment add_class(environment const &env, name const &n, bool persistent) {
-    return static_cast<basic_attribute const &>(get_system_attribute(*g_class_attr_name)).set(env, get_global_ios(), n, LEAN_DEFAULT_PRIORITY, persistent);
-}
+bool is_class_out_param(expr const & e) { return is_out_param_core(e.to_obj_arg()); }
+bool has_class_out_params(environment const & env, name const & c) { return has_out_params_core(env.to_obj_arg(), c.to_obj_arg()); }
+bool is_class(environment const & env, name const & c) { return is_class_core(env.to_obj_arg(), c.to_obj_arg()); }
+bool is_instance(environment const & env, name const & i) { return is_instance_core(env.to_obj_arg(), i.to_obj_arg()); }
+names get_class_instances(environment const & env, name const & c) { return names(get_class_instances_core(env.to_obj_arg(), c.to_obj_arg())); }
 
 environment add_instance(environment const & env, name const & n, bool persistent) {
-    return static_cast<basic_attribute const &>(get_system_attribute(*g_instance_attr_name)).set(env, get_global_ios(), n, LEAN_DEFAULT_PRIORITY, persistent);
+    if (!persistent) throw exception("local instances have been disabled");
+    return get_except_value<environment>(add_instance_core(env.to_obj_arg(), n.to_obj_arg()));
 }
 
 static name * g_anonymous_inst_name_prefix = nullptr;
@@ -237,35 +45,12 @@ bool is_anonymous_inst_name(name const & n) {
                    strlen(g_anonymous_inst_name_prefix->get_string().data())) == 0;
 }
 
-bool is_class_out_param(expr const & e) {
-    return is_app_of(e, get_out_param_name(), 1);
-}
 
 void initialize_class() {
-    g_class_attr_name = new name("class");
-    g_instance_attr_name = new name("instance");
-    g_class_name = new name("class");
-    class_ext::initialize();
-
-    register_system_attribute(basic_attribute(*g_class_attr_name, "type class",
-                                              [](environment const & env, io_state const &, name const & d, unsigned,
-                                                 bool persistent) {
-                                                  return add_class_core(env, d, persistent);
-                                             }));
-
-    register_system_attribute(basic_attribute(*g_instance_attr_name, "type class instance",
-                                              [](environment const & env, io_state const &, name const & d,
-                                                 unsigned, bool persistent) {
-                                                  return add_instance_core(env, d, persistent);
-                                              }));
-
     g_anonymous_inst_name_prefix = new name("_inst");
 }
 
 void finalize_class() {
-    class_ext::finalize();
-    delete g_class_name;
-    delete g_class_attr_name;
     delete g_anonymous_inst_name_prefix;
 }
 }
diff --git a/src/util/object_ref.h b/src/util/object_ref.h
index 413274298f..2b1a7e4335 100644
--- a/src/util/object_ref.h
+++ b/src/util/object_ref.h
@@ -192,4 +192,18 @@ inline object * mk_except_error_string(char const * err) {
     cnstr_set(r, 0, mk_string(err));
     return r;
 }
+
+/* Given `o` representing a Lean value of type `Except String A`, return `T` an smart pointer
+   that encapsulates `A` values or throw an exception */
+template<typename T> T get_except_value(obj_arg o) {
+    if (cnstr_tag(o) == 1) {
+        T result(cnstr_get(o, 0), true);
+        dec(o);
+        return result;
+    } else {
+        std::string err = string_to_std(cnstr_get(o, 0));
+        dec(o);
+        throw exception(err);
+    }
+}
 }