diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index 4f8ef15aa..24367962c 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -1,9 +1,10 @@
 add_library(kernel level.cpp diff_cnstrs.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp occurs.cpp replace_fn.cpp free_vars.cpp abstract.cpp
-instantiate.cpp context.cpp formatter.cpp max_sharing.cpp
-# normalizer.cpp object.cpp environment.cpp
+instantiate.cpp context.cpp formatter.cpp max_sharing.cpp kernel_exception.cpp
+object.cpp environment.cpp
+# normalizer.cpp
 # type_checker.cpp kernel.cpp metavar.cpp
-# justification.cpp unification_constraint.cpp kernel_exception.cpp
+# justification.cpp unification_constraint.cpp
 # type_checker_justification.cpp pos_info_provider.cpp
 # replace_visitor.cpp update_expr.cpp io_state.cpp
 # universe_constraints.cpp
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 465f2ed43..2b3f006cd 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -22,10 +22,8 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/environment.h"
 #include "kernel/threadsafe_environment.h"
-#include "kernel/type_checker.h"
-#include "kernel/normalizer.h"
-#include "kernel/universe_constraints.h"
-#include "kernel/kernel.h"
+// #include "kernel/type_checker.h"
+// #include "kernel/normalizer.h"
 #include "version.h"
 
 namespace lean {
@@ -182,7 +180,7 @@ unsigned environment_cell::get_max_weight(expr const & e) {
         }
         return true;
         };
-    for_each_fn<decltype(proc)> visitor(proc);
+    for_each_fn visitor(proc);
     visitor(e);
     return w;
 }
@@ -192,12 +190,12 @@ void environment_cell::check_name_core(name const & n) {
     if (has_parent())
         m_parent->check_name_core(n);
     if (m_object_dictionary.find(n) != m_object_dictionary.end())
-        throw already_declared_exception(env(), n);
+        throw_already_declared(env(), n);
 }
 
 void environment_cell::check_name(name const & n) {
     if (has_children())
-        throw read_only_environment_exception(env());
+        throw_read_only_environment(env());
     check_name_core(n);
 }
 
@@ -229,177 +227,17 @@ object environment_cell::get_object(name const & n) const {
     if (obj) {
         return *obj;
     } else {
-        throw unknown_object_exception(env(), n);
+        throw_unknown_object(env(), n);
     }
 }
 
-class universes {
-public:
-    std::vector<level>                  m_uvars;
-    universe_constraints                m_constraints;
-};
-
-universes & environment_cell::get_rw_universes() {
-    if (!m_universes) {
-        lean_assert(has_parent());
-        m_universes.reset(new universes(m_parent->get_rw_universes()));
-    }
-    return *m_universes;
-}
-
-universes const & environment_cell::get_ro_universes() const {
-    if (m_universes) {
-        return *m_universes;
-    } else {
-        lean_assert(has_parent());
-        return m_parent->get_ro_universes();
-    }
-}
-
-universe_constraints & environment_cell::get_rw_ucs() {
-    return get_rw_universes().m_constraints;
-}
-
-universe_constraints const & environment_cell::get_ro_ucs() const {
-    return get_ro_universes().m_constraints;
-}
-
-optional<int> environment_cell::get_universe_distance(name const & u1, name const & u2) const {
-    return get_ro_ucs().get_distance(u1, u2);
-}
-
-/** \brief Return true iff l1 >= l2 + k by asserted universe constraints. */
-bool environment_cell::is_ge(level const & l1, level const & l2, int k) const {
-    if (l1 == l2)
-        return k <= 0;
-    switch (kind(l2)) {
-    case level_kind::UVar:
-        switch (kind(l1)) {
-        case level_kind::UVar: return get_ro_ucs().is_implied(uvar_name(l1), uvar_name(l2), k);
-        case level_kind::Lift: return is_ge(lift_of(l1), l2, safe_sub(k, lift_offset(l1)));
-        case level_kind::Max:  return std::any_of(max_begin_levels(l1), max_end_levels(l1), [&](level const & l) { return is_ge(l, l2, k); });
-        }
-    case level_kind::Lift: return is_ge(l1, lift_of(l2), safe_add(k, lift_offset(l2)));
-    case level_kind::Max:  return std::all_of(max_begin_levels(l2), max_end_levels(l2), [&](level const & l) { return is_ge(l1, l, k); });
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
-/** \brief Return true iff l1 >= l2 is implied by asserted universe constraints. */
-bool environment_cell::is_ge(level const & l1, level const & l2) const {
-    return is_ge(l1, l2, 0);
-}
-
-/** \brief Add a new universe variable */
-level environment_cell::add_uvar_core(name const & n) {
-    check_name(n);
-    universes & u = get_rw_universes();
-    u.m_constraints.add_var(n);
-    level r(n);
-    u.m_uvars.push_back(r);
-    return r;
-}
-
 /**
-   \brief Add all basic constraints implied by n >= l + k
-
-   A basic constraint is a constraint of the form u >= v + k
-   where u and v are universe variables.
+   The kernel should *not* accept expressions containing Local or Meta.
+   Reason: they may introduce unsoundness.
 */
-void environment_cell::add_constraints(name const & n, level const & l, int k) {
-    switch (kind(l)) {
-    case level_kind::UVar: get_rw_ucs().add_constraint(n, uvar_name(l), k); return;
-    case level_kind::Lift: add_constraints(n, lift_of(l), safe_add(k, lift_offset(l))); return;
-    case level_kind::Max:  std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { add_constraints(n, l1, k); }); return;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
-/**
-   \brief Check if n >= l + k is consistent with the existing constraints.
-*/
-void environment_cell::check_consistency(name const & n, level const & l, int k) const {
-    switch (kind(l)) {
-    case level_kind::UVar:
-        if (l == ty_level(TypeU))
-            throw kernel_exception(env(), sstream() << "invalid universe constraint: " << n << " >= " << l << " + " << k
-                                   << ", several modules in Lean assume that " << l << " is the maximal universe");
-        if (!get_ro_ucs().is_consistent(n, uvar_name(l), k))
-            throw kernel_exception(env(), sstream() << "universe constraint inconsistency: " << n << " >= " << l << " + " << k);
-        if (get_ro_ucs().overflows(n, uvar_name(l), k))
-            throw kernel_exception(env(), sstream() << "universe constraint produces an integer overflow: " << n << " >= " << l << " + " << k);
-        return;
-    case level_kind::Lift: check_consistency(n, lift_of(l), safe_add(k, lift_offset(l))); return;
-    case level_kind::Max:  std::for_each(max_begin_levels(l), max_end_levels(l), [&](level const & l1) { check_consistency(n, l1, k); }); return;
-    }
-    lean_unreachable(); // LCOV_EXCL_LINE
-}
-
-/** \brief Add a new universe variable with constraint n >= l */
-level environment_cell::add_uvar_cnstr(name const & n, level const & l) {
-    if (has_children())
-        throw read_only_environment_exception(env());
-    level r;
-    auto const & uvs = get_ro_universes().m_uvars;
-    auto it = std::find_if(uvs.begin(), uvs.end(), [&](level const & l) { return uvar_name(l) == n; });
-    bool new_universe;
-    check_consistency(n, l, 0);
-    if (it == uvs.end()) {
-        r = add_uvar_core(n);
-        new_universe = true;
-    } else {
-        // universe n already exists, we must check consistency of the new constraint.
-        r = *it;
-        new_universe = false;
-    }
-    m_objects.push_back(mk_uvar_cnstr(n, l));
-    add_constraints(n, l, 0);
-    name const & Uname = uvar_name(ty_level(TypeU));
-    if (new_universe && n != Uname && !is_ge(ty_level(TypeU), r, 1)) {
-        // In Lean, U is the maximal universe, several Lean modules assume that,
-        // and the kernel axioms are all with respect to U.
-        // So, we force all other universes to smaller than U
-        add_uvar_cnstr(Uname, r+1);
-    }
-    return r;
-}
-
-/**
-   \brief Return the universe variable with given name. Throw an
-   exception if the environment and its ancestors do not
-   contain a universe variable named \c n.
-*/
-level environment_cell::get_uvar(name const & n) const {
-    auto const & uvs = get_ro_universes().m_uvars;
-    auto it = std::find_if(uvs.begin(), uvs.end(), [&](level const & l) { return uvar_name(l) == n; });
-    if (it == uvs.end())
-        throw unknown_universe_variable_exception(env(), n);
-    else
-        return *it;
-}
-
-/**
-   \brief Initialize the set of universe variables with bottom
-*/
-void environment_cell::init_uvars() {
-    m_universes.reset(new universes());
-    universes & u = get_rw_universes();
-    level bottom;
-    u.m_uvars.push_back(bottom);
-    u.m_constraints.add_var(uvar_name(bottom));
-}
-
-/**
-   The kernel should *not* accept expressions containing cached types.
-   Reason: Cached types may introduce unsoundness.
-   For example, in the environment env, the constant x may have type T.
-   Now suppose we are trying to add a new definition D that contains x,
-   and x is associated with a cached type T'. The cached type may allow
-   us to accept a definition that is type incorrect with respect to env.
-*/
-void environment_cell::check_no_cached_type(expr const & e) {
-    if (find(e, [](expr const & a) { return is_constant(a) && const_type(a); }))
-        throw kernel_exception(env(), "expression has a constant with a cached type, this is a bug in one of Lean tactics and/or solvers"); // LCOV_EXCL_LINE
+void environment_cell::check_no_mlocal(expr const & e) {
+    if (find(e, [](expr const & a, unsigned) { return is_mlocal(a); }))
+        throw_kernel_exception(env(), "expression has metavariable and/or local constants, this is a bug in one of Lean tactics and/or solvers"); // LCOV_EXCL_LINE
 }
 
 /**
@@ -407,12 +245,21 @@ void environment_cell::check_no_cached_type(expr const & e) {
    v is not convertible to \c t.
 */
 void environment_cell::check_type(name const & n, expr const & t, expr const & v) {
+#if 0
     if (m_type_check) {
         m_type_checker->check_type(t);
         expr v_t = m_type_checker->check(v);
         if (!m_type_checker->is_convertible(v_t, t))
             throw def_type_mismatch_exception(env(), n, t, v, v_t);
     }
+#endif
+}
+
+void environment_cell::check_type(expr const & t) {
+#if 0
+    if (m_type_check)
+        m_type_checker->check_type(t);
+#endif
 }
 
 /** \brief Throw exception if it is not a valid new definition */
@@ -421,34 +268,10 @@ void environment_cell::check_new_definition(name const & n, expr const & t, expr
     check_type(n, t, v);
 }
 
-/** \brief Add a new builtin value to this environment */
-void environment_cell::add_builtin(expr const & v) {
-    if (!is_value(v))
-        throw invalid_builtin_value_declaration(env(), v); // LCOV_EXCL_LINE
-    name const & n = to_value(v).get_name();
-    check_name(n);
-    name const & u = to_value(v).get_unicode_name();
-    check_name(u);
-    register_named_object(mk_builtin(v));
-    if (u != n) {
-        auxiliary_section([&]() {
-                add_definition(u, to_value(v).get_type(), mk_constant(n), false);
-            });
-    }
-}
-
-/** \brief Add a new builtin value set to this environment */
-void environment_cell::add_builtin_set(expr const & r) {
-    if (!is_value(r))
-        throw invalid_builtin_value_declaration(env(), r); // LCOV_EXCL_LINE
-    check_name(to_value(r).get_name());
-    register_named_object(mk_builtin_set(r));
-}
-
 /** \brief Add new definition. */
 void environment_cell::add_definition(name const & n, expr const & t, expr const & v, bool opaque) {
-    check_no_cached_type(t);
-    check_no_cached_type(v);
+    check_no_mlocal(t);
+    check_no_mlocal(v);
     check_new_definition(n, t, v);
     unsigned w = get_max_weight(v) + 1;
     register_named_object(mk_definition(n, t, v, w));
@@ -461,13 +284,15 @@ void environment_cell::add_definition(name const & n, expr const & t, expr const
    The type of the new definition is the type of \c v.
 */
 void environment_cell::add_definition(name const & n, expr const & v, bool opaque) {
-    check_no_cached_type(v);
+    check_no_mlocal(v);
     check_name(n);
     expr v_t;
+#if 0
     if (m_type_check)
         v_t = m_type_checker->check(v);
     else
         v_t = m_type_checker->infer_type(v);
+#endif
     unsigned w = get_max_weight(v) + 1;
     register_named_object(mk_definition(n, v_t, v, w));
     if (opaque)
@@ -476,8 +301,8 @@ void environment_cell::add_definition(name const & n, expr const & v, bool opaqu
 
 /** \brief Add new theorem. */
 void environment_cell::add_theorem(name const & n, expr const & t, expr const & v) {
-    check_no_cached_type(t);
-    check_no_cached_type(v);
+    check_no_mlocal(t);
+    check_no_mlocal(v);
     check_new_definition(n, t, v);
     register_named_object(mk_theorem(n, t, v));
 }
@@ -485,26 +310,24 @@ void environment_cell::add_theorem(name const & n, expr const & t, expr const &
 void environment_cell::set_opaque(name const & n, bool opaque) {
     auto obj = find_object(n);
     if (!obj || !obj->is_definition())
-        throw kernel_exception(env(), sstream() << "set_opaque failed, '" << n << "' is not a definition");
+        throw_kernel_exception(env(), sstream() << "set_opaque failed, '" << n << "' is not a definition");
     obj->set_opaque(opaque);
     add_neutral_object(new set_opaque_command(n, opaque));
 }
 
 /** \brief Add new axiom. */
 void environment_cell::add_axiom(name const & n, expr const & t) {
-    check_no_cached_type(t);
+    check_no_mlocal(t);
     check_name(n);
-    if (m_type_check)
-        m_type_checker->check_type(t);
+    check_type(t);
     register_named_object(mk_axiom(n, t));
 }
 
 /** \brief Add new variable. */
 void environment_cell::add_var(name const & n, expr const & t) {
-    check_no_cached_type(t);
+    check_no_mlocal(t);
     check_name(n);
-    if (m_type_check)
-        m_type_checker->check_type(t);
+    check_type(t);
     register_named_object(mk_var_decl(n, t));
 }
 
@@ -532,20 +355,36 @@ object const & environment_cell::get_object(unsigned i, bool local) const {
     }
 }
 
-expr environment_cell::type_check(expr const & e, context const & ctx) const {
+expr environment_cell::type_check(expr const & e) const {
+#if 0
     return m_type_checker->check(e, ctx);
+#else
+    return e;
+#endif
 }
 
-expr environment_cell::infer_type(expr const & e, context const & ctx) const {
+expr environment_cell::infer_type(expr const & e) const {
+#if 0
     return m_type_checker->infer_type(e, ctx);
+#else
+    return e;
+#endif
 }
 
-expr environment_cell::normalize(expr const & e, context const & ctx, bool unfold_opaque) const {
+expr environment_cell::normalize(expr const & e) const {
+#if 0
     return m_type_checker->get_normalizer()(e, ctx, unfold_opaque);
+#else
+    return e;
+#endif
 }
 
-bool environment_cell::is_proposition(expr const & e, context const & ctx) const {
+bool environment_cell::is_proposition(expr const & e) const {
+#if 0
     return m_type_checker->is_proposition(e, ctx);
+#else
+    return false;
+#endif
 }
 
 bool environment_cell::already_imported(name const & n) const {
@@ -561,7 +400,7 @@ bool environment_cell::mark_imported_core(name n) {
     if (already_imported(n)) {
         return false;
     } else if (has_children()) {
-        throw read_only_environment_exception(env());
+        throw_read_only_environment(env());
     } else {
         m_imported_modules.insert(n);
         return true;
@@ -618,12 +457,12 @@ bool environment_cell::load_core(std::string const & fname, io_state const & ios
     if (!mod_name || mark_imported_core(fname)) {
         std::ifstream in(fname, std::ifstream::binary);
         if (!in.good())
-            throw exception(sstream() << "failed to open file '" << fname << "'");
+            throw_kernel_exception(env(), sstream() << "failed to open file '" << fname << "'");
         deserializer d(in);
         std::string header;
         d >> header;
         if (header != g_olean_header)
-            throw exception(sstream() << "file '" << fname << "' does not seem to be a valid object Lean file");
+            throw_kernel_exception(env(), sstream() << "file '" << fname << "' does not seem to be a valid object Lean file");
         unsigned major, minor;
         // Perhaps we should enforce the right version number
         d >> major >> minor;
@@ -672,7 +511,6 @@ environment_cell::environment_cell():
     m_num_children(0) {
     m_trust_imported = false;
     m_type_check     = true;
-    init_uvars();
 }
 
 environment_cell::environment_cell(std::shared_ptr<environment_cell> const & parent):
@@ -691,14 +529,18 @@ environment_cell::~environment_cell() {
 environment::environment():
     m_ptr(std::make_shared<environment_cell>()) {
     m_ptr->m_this = m_ptr;
+#if 0
     m_ptr->m_type_checker.reset(new type_checker(*this));
+#endif
 }
 
 // used when creating a new child environment
 environment::environment(std::shared_ptr<environment_cell> const & parent, bool):
     m_ptr(std::make_shared<environment_cell>(parent)) {
     m_ptr->m_this = m_ptr;
+#if 0
     m_ptr->m_type_checker.reset(new type_checker(*this));
+#endif
 }
 
 // used when creating a reference to the parent environment
@@ -712,7 +554,7 @@ ro_environment::ro_environment(environment const & env):
 
 ro_environment::ro_environment(weak_ref const & r) {
     if (r.expired())
-        throw exception("weak reference to environment object has expired (i.e., the environment has been deleted)");
+        throw_kernel_exception(*this, "weak reference to environment object has expired (i.e., the environment has been deleted)");
     m_ptr = r.lock();
 }
 
@@ -750,26 +592,4 @@ read_write_shared_environment::read_write_shared_environment(environment const &
     m_lock(m_env.m_ptr->m_mutex) {
 }
 read_write_shared_environment::~read_write_shared_environment() {}
-
-static std::unique_ptr<name_map<std::pair<mk_builtin_fn, bool>>> g_available_builtins;
-name_map<std::pair<mk_builtin_fn, bool>> & get_available_builtins() {
-    if (!g_available_builtins)
-        g_available_builtins.reset(new name_map<std::pair<mk_builtin_fn, bool>>());
-    return *g_available_builtins;
-}
-
-void register_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set) {
-    auto & bs = get_available_builtins();
-    if (bs.find(n) != bs.end())
-        throw exception("invalid builtin object, system already has a builtin object with the given name"); // LCOV_EXCL_LINE
-    bs[n] = mk_pair(mk, is_builtin_set);
-}
-
-optional<std::pair<expr, bool>> get_builtin(name const & n) {
-    auto it = get_available_builtins().find(n);
-    if (it != get_available_builtins().end())
-        return optional<std::pair<expr, bool>>(it->second.first(), it->second.second);
-    else
-        return optional<std::pair<expr, bool>>();
-}
 }
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 4dad4418b..9cf1e8e36 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -14,7 +14,6 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "util/shared_mutex.h"
 #include "util/name_map.h"
-#include "kernel/context.h"
 #include "kernel/object.h"
 #include "kernel/level.h"
 
@@ -23,8 +22,6 @@ class environment;
 class ro_environment;
 class type_checker;
 class environment_extension;
-class universe_constraints;
-class universes;
 
 /** \brief Implementation of the Lean environment. */
 class environment_cell {
@@ -35,15 +32,14 @@ class environment_cell {
     typedef name_map<object> object_dictionary;
     typedef std::tuple<level, level, int> constraint;
     std::weak_ptr<environment_cell>         m_this;
-    // Universe variable management
-    std::unique_ptr<universes>              m_universes;
     // Children environment management
     atomic<unsigned>                        m_num_children;
     std::shared_ptr<environment_cell>       m_parent;
     // Object management
     std::vector<object>                     m_objects;
     object_dictionary                       m_object_dictionary;
-    std::unique_ptr<type_checker>           m_type_checker;
+
+    // std::unique_ptr<type_checker>           m_type_checker;
     std::set<name>                          m_imported_modules;   // set of imported files and builtin modules
     bool                                    m_trust_imported; // if true, then imported modules are not type checked.
     bool                                    m_type_check;     // auxiliary flag used to implement m_trust_imported.
@@ -69,18 +65,9 @@ class environment_cell {
     void register_named_object(object const & new_obj);
     optional<object> get_object_core(name const & n) const;
 
-    universes & get_rw_universes();
-    universes const & get_ro_universes() const;
-    universe_constraints & get_rw_ucs();
-    universe_constraints const & get_ro_ucs() const;
-
-    level add_uvar_core(name const & n);
-    bool is_ge(level const & l1, level const & l2, int k) const;
-    void check_consistency(name const & n, level const & l, int k) const;
-    void add_constraints(name const & n, level const & l, int k);
-    void init_uvars();
-    void check_no_cached_type(expr const & e);
+    void check_no_mlocal(expr const & e);
     void check_type(name const & n, expr const & t, expr const & v);
+    void check_type(expr const & t);
     void check_new_definition(name const & n, expr const & t, expr const & v);
 
     bool mark_imported_core(name n);
@@ -111,60 +98,9 @@ public:
     */
     environment mk_child() const;
 
-    // =======================================
-    // Universe variables
-    /**
-       \brief Add a new universe variable constraint of the form <tt>n >= l</tt>.
-       Return the level of \c n.
-
-       \remark An exception is thrown if a universe inconsistency is detected.
-    */
-    level add_uvar_cnstr(name const & n, level const & l);
-    level add_uvar_cnstr(name const & n) { return add_uvar_cnstr(n, level()); }
-
-    /**
-       \brief Return true iff the constraint l1 >= l2 is implied by the constraints
-       in the environment.
-    */
-    bool is_ge(level const & l1, level const & l2) const;
-
-    /**
-       \brief Return the (minimal) distance between two universes.
-       That is, the biggest \c k s.t. <tt>u1 >= u2 + k</tt>.
-       Return none if there is no such \c k.
-    */
-    optional<int> get_universe_distance(name const & u1, name const & u2) const;
-
-    /**
-       \brief Return universal variable with the given name.
-       Throw an exception if variable is not defined in this environment.
-    */
-    level get_uvar(name const & n) const;
-    // =======================================
-
     // =======================================
     // Environment Objects
 
-    /**
-        \brief Add builtin value to the environment.
-
-        \pre is_value(v)
-    */
-    void add_builtin(expr const & v);
-
-    /**
-       \brief Add a builtin value set to the environment.
-
-       The set is registered by providing a representative of the set.
-       Each builtin set of values is implemented by a C++ class.
-       The environment will only accept object of the same class of
-       the representative. This functionality is used to support
-       infinite set of builtin values such as the natural numbers.
-
-       \pre is_value(r);
-    */
-    void add_builtin_set(expr const & r);
-
     /**
        \brief Add a new definition n : t := v.
        It throws an exception if v does not have type t.
@@ -218,22 +154,22 @@ public:
     /**
        \brief Type check the given expression, and return the type of \c e in the given context and this environment.
     */
-    expr type_check(expr const & e, context const & ctx = context()) const;
+    expr type_check(expr const & e) const;
 
     /**
        \brief Return the type of \c e in the given context and this environment.
     */
-    expr infer_type(expr const & e, context const & ctx = context()) const;
+    expr infer_type(expr const & e) const;
 
     /**
        \brief Normalize \c e in the given context and this environment.
     */
-    expr normalize(expr const & e, context const & ctx = context(), bool unfold_opaque = false) const;
+    expr normalize(expr const & e) const;
 
     /**
        \brief Return true iff \c e is a proposition.
     */
-    bool is_proposition(expr const & e, context const & ctx = context()) const;
+    bool is_proposition(expr const & e) const;
 
     /**
        \brief Low-level function for accessing objects. Consider using iterators.
@@ -421,34 +357,17 @@ bool is_end_import(object const & obj);
 */
 optional<std::string> get_imported_module(object const & obj);
 
-typedef std::function<expr()> mk_builtin_fn;
 /**
-   \brief Register a builtin or builtin-set that is available to be added to
-   a Lean environment.
-*/
-void register_builtin(name const & n, mk_builtin_fn mk, bool is_builtin_set);
-struct register_builtin_fn {
-    register_builtin_fn(name const & n, mk_builtin_fn mk, bool is_builtin_set = false) {
-        register_builtin(n, mk, is_builtin_set);
-    }
-};
-/**
-   \brief Return a builtin/builtin-set associated with the name \c n.
-   Return none if there is no builtin associated the given name.
-*/
-optional<std::pair<expr, bool>> get_builtin(name const & n);
-
-/**
-   \brief Return true iff \c obj is a SetOpaque command mark.
+   \brief Return true iff \c obj is a set_opaque command mark.
 */
 bool is_set_opaque(object const & obj);
 /**
-   \brief Return the identifier of a SetOpaque command.
+   \brief Return the identifier of a set_opaque command.
    \pre is_set_opaque(obj)
 */
 name const & get_set_opaque_id(object const & obj);
 /**
-   \brief Return the flag of a SetOpaque command.
+   \brief Return the flag of a set_opaque command.
    \pre is_set_opaque(obj)
 */
 bool get_set_opaque_flag(object const & obj);
diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h
index af6be062a..44c9f7358 100644
--- a/src/kernel/formatter.h
+++ b/src/kernel/formatter.h
@@ -56,4 +56,6 @@ std::ostream & operator<<(std::ostream & out, expr const & e);
    \brief Create a simple formatter object based on operator<<
 */
 formatter mk_simple_formatter();
+
+typedef std::function<format(formatter const &, options const &)> pp_fn;
 }
diff --git a/src/kernel/kernel_exception.cpp b/src/kernel/kernel_exception.cpp
index 3a31ac54c..08d5b50ae 100644
--- a/src/kernel/kernel_exception.cpp
+++ b/src/kernel/kernel_exception.cpp
@@ -5,21 +5,68 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
+#include <string>
+#include "util/sstream.h"
 #include "kernel/kernel_exception.h"
 
 namespace lean {
-format kernel_exception::pp(formatter const &, options const &) const {
-    return format(what());
+format kernel_exception::pp(formatter const &, options const &) const { return format(what()); }
+
+class generic_kernel_exception : public kernel_exception {
+protected:
+    optional<expr> m_main_expr;
+    pp_fn          m_pp_fn;
+public:
+    generic_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m, pp_fn const & fn):
+        kernel_exception(env, msg),
+        m_main_expr(m),
+        m_pp_fn(fn) {}
+    virtual ~generic_kernel_exception() noexcept {}
+    virtual optional<expr> get_main_expr() const { return m_main_expr; }
+    virtual format pp(formatter const & fmt, options const & opts) const { return m_pp_fn(fmt, opts); }
+    virtual exception * clone() const { return new generic_kernel_exception(m_env, m_msg.c_str(), m_main_expr, m_pp_fn); }
+    virtual void rethrow() const { throw *this; }
+};
+
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m) {
+    std::string msg_str = msg;
+    throw generic_kernel_exception(env, msg, m, [=](formatter const &, options const &) { return format(msg); });
 }
 
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, sstream const & strm, optional<expr> const & m) {
+    throw_kernel_exception(env, strm.str().c_str(), m);
+}
+
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, pp_fn const & fn,
+                                           optional<expr> const & m) {
+    throw generic_kernel_exception(env, msg, m, fn);
+}
+
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional<expr> const & m) {
+    throw generic_kernel_exception(env, "kernel exception", m, fn);
+}
+
+[[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n) {
+    throw_kernel_exception(env, sstream() << "unknown object '" << n << "'");
+}
+
+[[ noreturn ]] void throw_already_declared(ro_environment const & env, name const & n) {
+    throw_kernel_exception(env, sstream() << "invalid object declaration, environment already has an object named '" << n << "'");
+}
+
+[[ noreturn ]] void throw_read_only_environment(ro_environment const & env) {
+    throw_kernel_exception(env, "environment cannot be updated because it has children environments");
+}
+
+
+#if 0
+
+
+
 format unknown_name_exception::pp(formatter const &, options const &) const {
     return format{format(what()), format(" '"), format(get_name()), format("'")};
 }
 
-format already_declared_exception::pp(formatter const &, options const &) const {
-    return format{format("invalid object declaration, environment already has an object named '"), format(get_name()), format("'")};
-}
-
 format has_no_type_exception::pp(formatter const &, options const &) const {
     return format{format("object '"), format(const_name(m_const)), format("' has no type associated with it")};
 }
@@ -107,4 +154,5 @@ format def_type_mismatch_exception::pp(formatter const & fmt, options const & op
     r += nest(indent, compose(line(), fmt(ctx, get_value_type(), false, opts)));
     return r;
 }
+#endif
 }
diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h
index 23507b85d..fe487c41c 100644
--- a/src/kernel/kernel_exception.h
+++ b/src/kernel/kernel_exception.h
@@ -34,65 +34,20 @@ public:
     virtual void rethrow() const { throw *this; }
 };
 
-/** \brief Base class for unknown universe or object exceptions. */
-class unknown_name_exception : public kernel_exception {
-protected:
-    name m_name;
-public:
-    unknown_name_exception(ro_environment const & env, name const & n):kernel_exception(env), m_name(n) {}
-    virtual ~unknown_name_exception() {}
-    name const & get_name() const { return m_name; }
-    virtual format pp(formatter const & fmt, options const & opts) const;
-    virtual exception * clone() const { return new unknown_name_exception(m_env, m_name); }
-    virtual void rethrow() const { throw *this; }
-};
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg, optional<expr> const & m = none_expr());
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, sstream const & strm,
+                                           optional<expr> const & m = none_expr());
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, char const * msg,
+                                           pp_fn const & fn, optional<expr> const & m = none_expr());
+[[ noreturn ]] void throw_kernel_exception(ro_environment const & env, pp_fn const & fn, optional<expr> const & m = none_expr());
 
-/** \brief Exception used to report that a universe variable is not known in a given environment. */
-class unknown_universe_variable_exception : public unknown_name_exception {
-public:
-    unknown_universe_variable_exception(ro_environment const & env, name const & n):unknown_name_exception(env, n) {}
-    virtual char const * what() const noexcept { return "unknown universe variable"; }
-    virtual exception * clone() const { return new unknown_universe_variable_exception(m_env, m_name); }
-    virtual void rethrow() const { throw *this; }
-};
+[[ noreturn ]] void throw_unknown_object(ro_environment const & env, name const & n);
+[[ noreturn ]] void throw_already_declared(ro_environment const & env, name const & n);
+[[ noreturn ]] void throw_read_only_environment(ro_environment const & env);
 
-/** \brief Exception used to report that an object is not known in a given environment. */
-class unknown_object_exception : public unknown_name_exception {
-public:
-    unknown_object_exception(ro_environment const & env, name const & n):unknown_name_exception(env, n) {}
-    virtual char const * what() const noexcept { return "unknown object"; }
-    virtual exception * clone() const { return new unknown_object_exception(m_env, m_name); }
-    virtual void rethrow() const { throw *this; }
-};
 
-/** \brief Base class for already declared object. */
-class already_declared_exception : public kernel_exception {
-protected:
-    name m_name;
-public:
-    already_declared_exception(ro_environment const & env, name const & n):kernel_exception(env), m_name(n) {}
-    virtual ~already_declared_exception() noexcept {}
-    name const & get_name() const { return m_name; }
-    virtual char const * what() const noexcept { return "invalid object declaration, environment already has an object with the given name"; }
-    virtual format pp(formatter const & fmt, options const & opts) const;
-    virtual exception * clone() const { return new already_declared_exception(m_env, m_name); }
-    virtual void rethrow() const { throw *this; }
-};
-
-/**
-    \brief Exception used to report that a update has been tried on a
-    read-only environment.
-
-    An environment is read-only if it has "children environments".
-*/
-class read_only_environment_exception : public kernel_exception {
-public:
-    read_only_environment_exception(ro_environment const & env):kernel_exception(env) {}
-    virtual char const * what() const noexcept { return "environment cannot be updated because it has children environments"; }
-    virtual exception * clone() const { return new read_only_environment_exception(m_env); }
-    virtual void rethrow() const { throw *this; }
-};
 
+#if 0
 /** \brief Base class for type checking related exceptions. */
 class type_checker_exception : public kernel_exception {
 public:
@@ -266,35 +221,6 @@ public:
     virtual void rethrow() const { throw *this; }
 };
 
-/**
-    \brief Invalid builtin value declaration.
-*/
-class invalid_builtin_value_declaration : public kernel_exception {
-    expr m_expr;
-public:
-    invalid_builtin_value_declaration(ro_environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
-    virtual ~invalid_builtin_value_declaration() {}
-    virtual char const * what() const noexcept { return "invalid builtin value declaration, expression is not a builtin value"; }
-    virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
-    virtual exception * clone() const { return new invalid_builtin_value_declaration(m_env, m_expr); }
-    virtual void rethrow() const { throw *this; }
-};
-
-/**
-    \brief Exception used to report that a builtin value is not
-    declared in the environment.
-*/
-class invalid_builtin_value_reference : public kernel_exception {
-    expr m_expr;
-public:
-    invalid_builtin_value_reference(ro_environment const & env, expr const & e):kernel_exception(env), m_expr(e) {}
-    virtual ~invalid_builtin_value_reference() {}
-    virtual char const * what() const noexcept { return "invalid builtin value reference, this kind of builtin value was not declared in the environment"; }
-    virtual optional<expr> get_main_expr() const { return some_expr(m_expr); }
-    virtual exception * clone() const { return new invalid_builtin_value_reference(m_env, m_expr); }
-    virtual void rethrow() const { throw *this; }
-};
-
 /**
    \brief Unexpected metavariable occurrence
 */
@@ -308,4 +234,5 @@ public:
     virtual exception * clone() const { return new unexpected_metavar_occurrence(m_env, m_expr); }
     virtual void rethrow() const { throw *this; }
 };
+#endif
 }
diff --git a/src/kernel/object.cpp b/src/kernel/object.cpp
index 9987b7788..e0f04c407 100644
--- a/src/kernel/object.cpp
+++ b/src/kernel/object.cpp
@@ -46,86 +46,6 @@ public:
     virtual name get_name() const { return m_name; }
 };
 
-/**
-   \brief Universe variable constraint.
-*/
-class uvar_constraint_object_cell : public named_object_cell {
-    level m_level;
-public:
-    uvar_constraint_object_cell(name const & n, level const & l):
-        named_object_cell(object_kind::UVarConstraint, n), m_level(l) {}
-    virtual ~uvar_constraint_object_cell() {}
-
-    virtual bool has_cnstr_level() const  { return true; }
-    virtual level get_cnstr_level() const { return m_level; }
-    virtual char const * keyword() const  { return "universe"; }
-    virtual void write(serializer & s) const { s << "universe" << get_name() << m_level; }
-};
-static void read_uvar_cnstr(environment const & env, io_state const &, deserializer & d) {
-    name n    = read_name(d);
-    level lvl = read_level(d);
-    env->add_uvar_cnstr(n, lvl);
-}
-static object_cell::register_deserializer_fn uvar_ds("universe", read_uvar_cnstr);
-
-/**
-   \brief Builtin object.
-*/
-class builtin_object_cell : public object_cell {
-    expr m_value;
-    bool m_opaque;
-public:
-    builtin_object_cell(expr const & v):
-        object_cell(object_kind::Builtin), m_value(v), m_opaque(false) { lean_assert(is_value(v)); }
-    virtual ~builtin_object_cell() {}
-    virtual bool has_name() const        { return true; }
-    virtual name get_name() const        { return to_value(m_value).get_name(); }
-    virtual bool has_type() const        { return true; }
-    virtual expr get_type() const        { return to_value(m_value).get_type(); }
-    virtual bool is_definition() const   { return true; }
-    virtual bool is_opaque() const       { return m_opaque; }
-    virtual void set_opaque(bool f)      { m_opaque = f; }
-    virtual expr get_value() const       { return m_value; }
-    virtual char const * keyword() const { return "builtin"; }
-    virtual bool is_builtin() const      { return true; }
-    virtual void write(serializer & s) const { s << "builtin" << m_value; }
-};
-static void read_builtin(environment const & env, io_state const &, deserializer & d) {
-    expr v      = read_expr(d);
-    env->add_builtin(v);
-}
-static object_cell::register_deserializer_fn builtin_ds("builtin", read_builtin);
-
-
-/**
-   \brief Base class for capturing a set of builtin objects such as
-      a) the natural numbers 0, 1, 2, ...
-      b) the integers 0, -1, 1, -2, 2, ...
-      c) the reals
-      d) ...
-   This object represents an infinite set of declarations.
-   This is just a markup to sign that an environment depends on a
-   particular builtin set of values.
-*/
-class builtin_set_object_cell : public object_cell {
-    // The representative is only used to test if a builtin value
-    // is in the same C++ class of the representative.
-    expr m_representative;
-public:
-    builtin_set_object_cell(expr const & r):object_cell(object_kind::BuiltinSet), m_representative(r) { lean_assert(is_value(r)); }
-    virtual ~builtin_set_object_cell() {}
-    virtual bool has_name() const { return true; }
-    virtual name get_name() const { return to_value(m_representative).get_name(); }
-    virtual bool is_builtin_set() const { return true; }
-    virtual bool in_builtin_set(expr const & v) const { return is_value(v) && typeid(to_value(v)) == typeid(to_value(m_representative)); }
-    virtual char const * keyword() const { return "builtinset"; }
-    virtual void write(serializer & s) const { s << "builtinset" << m_representative; }
-};
-static void read_builtin_set(environment const & env, io_state const &, deserializer & d) {
-    env->add_builtin_set(read_expr(d));
-}
-static object_cell::register_deserializer_fn builtin_set_ds("builtinset", read_builtin_set);
-
 /**
    \brief Named (and typed) kernel objects.
 */
@@ -233,11 +153,10 @@ static void read_theorem(environment const & env, io_state const &, deserializer
 }
 static object_cell::register_deserializer_fn theorem_ds("th", read_theorem);
 
-object mk_uvar_cnstr(name const & n, level const & l) { return object(new uvar_constraint_object_cell(n, l)); }
-object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight) { return object(new definition_object_cell(n, t, v, weight)); }
+object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight) {
+    return object(new definition_object_cell(n, t, v, weight));
+}
 object mk_theorem(name const & n, expr const & t, expr const & v) { return object(new theorem_object_cell(n, t, v)); }
 object mk_axiom(name const & n, expr const & t) { return object(new axiom_object_cell(n, t)); }
 object mk_var_decl(name const & n, expr const & t) { return object(new variable_decl_object_cell(n, t)); }
-object mk_builtin(expr const & v) { return object(new builtin_object_cell(v)); }
-object mk_builtin_set(expr const & r) { return object(new builtin_set_object_cell(r)); }
 }
diff --git a/src/kernel/object.h b/src/kernel/object.h
index c33c8fca6..a907ded39 100644
--- a/src/kernel/object.h
+++ b/src/kernel/object.h
@@ -18,7 +18,7 @@ Author: Leonardo de Moura
 namespace lean {
 class io_state;
 class object;
-enum class object_kind { UVarConstraint, Definition, Postulate, Builtin, BuiltinSet, Neutral };
+enum class object_kind { Definition, Postulate, Neutral };
 
 class object_cell {
 protected:
@@ -45,11 +45,6 @@ public:
     /** \brief Return object name. \pre has_name() */
     virtual name get_name() const { lean_unreachable(); } // LCOV_EXCL_LINE
 
-    /** \brief Has constraint level associated with it (for universal variables). */
-    virtual bool has_cnstr_level() const { return false; }
-    /** \brief Return the constraint level associated with the object. */
-    virtual level get_cnstr_level() const { lean_unreachable(); } // LCOV_EXCL_LINE
-
     /** \brief Return true iff object has a type. */
     virtual bool has_type() const { return false; }
     /** \brief Return object type. \pre has_type() */
@@ -63,13 +58,9 @@ public:
     virtual expr get_value() const { lean_unreachable(); } // LCOV_EXCL_LINE
 
     virtual bool is_axiom() const { return false; }
-    virtual bool is_builtin() const { return false; }
-    virtual bool is_builtin_set() const { return false; }
     virtual bool is_theorem() const { return false; }
     virtual bool is_var_decl() const { return false; }
 
-    virtual bool in_builtin_set(expr const &) const { return false; }
-
     virtual unsigned get_weight() const { return 0; }
 
     virtual void write(serializer & ) const = 0;
@@ -111,21 +102,16 @@ public:
 
     object_kind kind() const { return m_ptr->kind(); }
 
-    friend object mk_uvar_cnstr(name const & n, level const & l);
     friend object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
     friend object mk_theorem(name const & n, expr const & t, expr const & v);
     friend object mk_axiom(name const & n, expr const & t);
     friend object mk_var_decl(name const & n, expr const & t);
     friend object mk_neutral(neutral_object_cell * c);
-    friend object mk_builtin(expr const & v);
-    friend object mk_builtin_set(expr const & r);
 
     char const * keyword() const { return m_ptr->keyword(); }
     bool has_name() const { return m_ptr->has_name(); }
     name get_name() const { return m_ptr->get_name(); }
     bool has_type() const { return m_ptr->has_type(); }
-    bool has_cnstr_level() const { return m_ptr->has_cnstr_level(); }
-    level get_cnstr_level() const { return m_ptr->get_cnstr_level(); }
     expr get_type() const { return m_ptr->get_type(); }
     bool is_definition() const { return m_ptr->is_definition(); }
     bool is_opaque() const { return m_ptr->is_opaque(); }
@@ -135,12 +121,8 @@ public:
     bool is_axiom() const { return m_ptr->is_axiom(); }
     bool is_theorem() const { return m_ptr->is_theorem(); }
     bool is_var_decl() const { return m_ptr->is_var_decl(); }
-    bool is_builtin() const { return m_ptr->is_builtin(); }
-    bool is_builtin_set() const { return m_ptr->is_builtin_set(); }
-    bool in_builtin_set(expr const & e) const { return m_ptr->in_builtin_set(e); }
 
     void write(serializer & s) const { m_ptr->write(s); }
-
     object_cell const * cell() const { return m_ptr; }
 };
 
@@ -148,9 +130,6 @@ inline optional<object> none_object() { return optional<object>(); }
 inline optional<object> some_object(object const & o) { return optional<object>(o); }
 inline optional<object> some_object(object && o) { return optional<object>(std::forward<object>(o)); }
 
-object mk_uvar_cnstr(name const & n, level const & l);
-object mk_builtin(expr const & v);
-object mk_builtin_set(expr const & r);
 object mk_definition(name const & n, expr const & t, expr const & v, unsigned weight);
 object mk_theorem(name const & n, expr const & t, expr const & v);
 object mk_axiom(name const & n, expr const & t);