diff --git a/library/init/lean/elaborator.lean b/library/init/lean/elaborator.lean
index 2f372bb6a0..3d6d6299b1 100644
--- a/library/init/lean/elaborator.lean
+++ b/library/init/lean/elaborator.lean
@@ -27,7 +27,7 @@ namespace elaborator
 -- TODO(Sebastian): should be its own monad?
 structure name_generator :=
 («prefix» : name)
-(next_idx : nat) -- TODO(Sebastian): uint32
+(next_idx : uint32)
 
 structure section_var :=
 (uniq_name : name)
diff --git a/src/frontends/lean/vm_elaborator.cpp b/src/frontends/lean/vm_elaborator.cpp
index 8bff5d44e0..afdeb68065 100644
--- a/src/frontends/lean/vm_elaborator.cpp
+++ b/src/frontends/lean/vm_elaborator.cpp
@@ -420,181 +420,25 @@ static void elaborate_command(parser & p, expr const & cmd) {
 /* TEMPORARY code for the old runtime */
 
 
-struct vm_env : public vm_external {
+struct lean_environment : public external_object {
     environment m_env;
 
-    explicit vm_env(environment const & env) : m_env(env) {}
-
-    virtual ~vm_env() {}
-
-    virtual void dealloc() override { delete this; }
-
-    virtual vm_external *ts_clone(vm_clone_fn const &) override { lean_unreachable(); }
-
-    virtual vm_external *clone(vm_clone_fn const &) override { lean_unreachable(); }
+    explicit lean_environment(environment const & env) : m_env(env) {}
+    virtual ~lean_environment() {}
 };
 
-environment const & to_env(vm_obj const & o) {
-    lean_vm_check(dynamic_cast<vm_env *>(to_external(o)));
-    return static_cast<vm_env *>(to_external(o))->m_env;
+environment const & to_env(b_obj_arg o) {
+    // lean_assert(dynamic_cast<lean_environment *>(to_external(o)));
+    return static_cast<lean_environment *>(to_external(o))->m_env;
 }
 
-vm_obj vm_environment_mk_empty(vm_obj const&) {
-    return mk_vm_external(new vm_env(environment()));
+obj_res to_lean_environment(environment const & env) {
+    return new(alloc_heap_object(sizeof(lean_environment))) lean_environment(env);
 }
 
-name to_name(vm_obj const & o) {
-    switch (cidx(o)) {
-        case 0: return name();
-        case 1: {
-            std::string str = to_string(cfield(o, 1));
-            return name(to_name(cfield(o, 0)), str.c_str());
-        }
-        case 2:
-            return name(to_name(cfield(o, 0)), nat(vm_nat_to_mpz1(cfield(o, 1))));
-        default: lean_unreachable();
-    }
-}
-
-vm_obj vm_environment_contains(vm_obj const & vm_env, vm_obj const & vm_n) {
-    return mk_vm_simple(static_cast<bool>(to_env(vm_env).find(to_name(vm_n))));
-}
-
-vm_obj to_obj(name const & n) {
-    if (n.is_anonymous()) {
-        return mk_vm_simple(0);
-    } else if (n.is_string()) {
-        return mk_vm_constructor(1, to_obj(n.get_prefix()), to_obj(n.get_string().to_std_string()));
-    } else {
-        return mk_vm_constructor(2, to_obj(n.get_prefix()), mk_vm_nat(n.get_numeral().to_mpz()));
-    }
-}
-
-level to_level(vm_obj const & o) {
-    switch (cidx(o)) {
-        case 0:
-            return mk_level_zero();
-        case 1:
-            return mk_succ(to_level(cfield(o, 0)));
-        case 2:
-            return mk_max(to_level(cfield(o, 0)), to_level(cfield(o, 1)));
-        case 3:
-            return mk_imax(to_level(cfield(o, 0)), to_level(cfield(o, 1)));
-        case 4:
-            return mk_univ_param(to_name(cfield(o, 0)));
-        case 5:
-            return mk_univ_mvar(to_name(cfield(o, 0)));
-        default: lean_unreachable();
-    }
-}
-
-levels to_levels(vm_obj const & o) {
-    switch (cidx(o)) {
-        case 0:
-            return levels();
-        case 1:
-            return levels(to_level(cfield(o, 0)), to_levels(cfield(o, 1)));
-        default: lean_unreachable();
-    }
-}
-
-binder_info to_binder_info(vm_obj const & o) {
-    lean_assert(is_simple(o));
-    return static_cast<binder_info>(cidx(o));
-}
-
-vm_obj to_obj(binder_info const & bi) {
-    return mk_vm_simple(static_cast<unsigned>(bi));
-}
-
-kvmap to_kvmap(vm_obj const & o) {
-    switch (cidx(o)) {
-        case 0:
-            return kvmap();
-        case 1: {
-            auto vm_k = cfield(cfield(o, 0), 0);
-            auto vm_v = cfield(cfield(o, 0), 1);
-            auto vm_d = cfield(vm_v, 0);
-            data_value v;
-            switch (cidx(vm_v)) {
-                case 0:
-                    v = data_value(to_string(vm_d));
-                    break;
-                case 1:
-                    v = data_value(nat(vm_nat_to_mpz1(vm_d)));
-                    break;
-                case 2:
-                    v = data_value(to_bool(vm_d));
-                    break;
-                case 3:
-                    v = data_value(to_name(vm_d));
-                    break;
-                default: lean_unreachable();
-            }
-            return kvmap({to_name(vm_k), v}, to_kvmap(cfield(o, 1)));
-        }
-        default: lean_unreachable();
-    }
-}
-
-// I really don't want to deal with the reverse translation right now
-struct vm_expr : public vm_external {
-    expr m_expr;
-    explicit vm_expr(expr const & expr) : m_expr(expr) {}
-    virtual ~vm_expr() {}
-    virtual void dealloc() override { delete this; }
-    virtual vm_external *ts_clone(vm_clone_fn const &) override { lean_unreachable(); }
-    virtual vm_external *clone(vm_clone_fn const &) override { lean_unreachable(); }
-};
-
-expr to_expr(vm_obj const & o) {
-    if (is_external(o)) {
-        lean_vm_check(dynamic_cast<vm_expr *>(to_external(o)));
-        return static_cast<vm_expr *>(to_external(o))->m_expr;
-    }
-
-    switch (cidx(o)) {
-        case 0:
-            return mk_bvar(nat(vm_nat_to_mpz1(cfield(o, 0))));
-        case 1:
-            return mk_local(to_name(cfield(o, 0)), to_name(cfield(o, 1)), to_expr(cfield(o, 2)), to_binder_info(cfield(o, 3)));
-        case 2:
-            return mk_metavar(to_name(cfield(o, 0)), to_expr(cfield(o, 1)));
-        case 3:
-            return mk_sort(to_level(cfield(o, 0)));
-        case 4:
-            return mk_constant(to_name(cfield(o, 0)), to_levels(cfield(o, 1)));
-        case 5:
-            return mk_app(to_expr(cfield(o, 0)), to_expr(cfield(o, 1)));
-        case 6:
-            return mk_lambda(to_name(cfield(o, 0)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3)),
-                             to_binder_info(cfield(o, 1)));
-        case 7:
-            return mk_pi(to_name(cfield(o, 0)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3)),
-                         to_binder_info(cfield(o, 1)));
-        case 8:
-            return mk_let(to_name(cfield(o, 0)), to_expr(cfield(o, 1)), to_expr(cfield(o, 2)), to_expr(cfield(o, 3)));
-        case 9: {
-            auto l = cfield(o, 0);
-            switch (cidx(l)) {
-                case 0:
-                    return mk_lit(literal(to_string(cfield(l, 0)).c_str()));
-                case 1:
-                    return mk_lit(literal(vm_nat_to_mpz1(cfield(l, 0))));
-                default: lean_unreachable();
-            }
-        }
-        case 10:
-            return mk_mdata(to_kvmap(cfield(o, 0)), to_expr(cfield(o, 1)));
-        case 11:
-            return mk_proj(to_name(cfield(o, 0)), nat(vm_nat_to_mpz1(cfield(o, 1))), to_expr(cfield(o, 2)));
-        default: lean_unreachable();
-    }
-}
-
-options to_options(vm_obj o) {
+options to_options(b_obj_arg o) {
     options opts;
-    kvmap m = to_kvmap(o);
+    kvmap m = kvmap(o, true);
     for (auto const & kv : m) {
         switch (kv.snd().kind()) {
             case data_value_kind::Bool:
@@ -614,87 +458,71 @@ options to_options(vm_obj o) {
     return opts;
 }
 
-name_set to_name_set(vm_obj o) {
+name_set to_name_set(b_obj_arg o) {
     name_set ns;
-    while (o.is_ptr()) {
-        ns.insert(to_name(cfield(o, 0)));
-        o = cfield(o, 1);
+    names l(o, true);
+    for (auto const & n : l) {
+        ns.insert(n);
     }
     return ns;
 }
 
-name_generator to_name_generator(vm_obj const & o) {
+name_generator to_name_generator(b_obj_arg o) {
     name_generator ngen;
-    ngen.m_prefix = to_name(cfield(o, 0));
-    ngen.m_next_idx = to_unsigned(cfield(o, 1));
+    ngen.m_prefix = name(cnstr_get(o, 0), true);
+    ngen.m_next_idx = cnstr_get_scalar<uint32>(o, sizeof(void*));
     return ngen;
 }
 
-vm_obj to_obj(name_generator const & ngen) {
-    return mk_vm_constructor(0, to_obj(ngen.m_prefix), mk_vm_nat(ngen.m_next_idx));
-}
-
-vm_obj to_obj(pos_info const & pos) {
-    return mk_vm_constructor(0, mk_vm_simple(pos.first), mk_vm_simple(pos.second));
-}
-
-vm_obj to_obj(message const & msg) {
-    return mk_vm_constructor(0, {
-            to_obj(msg.get_filename()),
-            to_obj(msg.get_pos()),
-            msg.get_end_pos() ? to_obj(*msg.get_end_pos()) : mk_vm_none(),
-            mk_vm_simple(static_cast<unsigned>(msg.get_severity())),
-            to_obj(msg.get_caption()),
-            to_obj(msg.get_text()),
-    });
-}
-
-vm_obj to_obj(message_log const & log) {
-    auto msgs = log.to_buffer();
-    auto o = mk_vm_simple(0);
-    for (auto const & msg : msgs)
-        o = mk_vm_constructor(1, to_obj(msg), o);
+object_ref to_obj(name_generator const & ngen) {
+    auto o = mk_cnstr(0, ngen.m_prefix, sizeof(uint32 ));
+    cnstr_set_scalar(o.raw(), sizeof(void*), ngen.m_next_idx);
     return o;
 }
 
+extern "C" obj_res lean_environment_mk_empty(b_obj_arg) {
+    return to_lean_environment(environment());
+}
+
+extern "C" uint8 lean_environment_contains(b_obj_arg lean_environment, b_obj_arg vm_n) {
+    return static_cast<uint8>(static_cast<bool>(to_env(lean_environment).find(name(vm_n, true))));
+}
+
 /* elaborate_command (filename : string) : expr → old_elaborator_state → option old_elaborator_state × message_log */
 // TODO(Sebastian): replace `string` with `message` in the new runtime
-vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, vm_obj const & vm_st) {
-    auto vm_e = cfield(vm_st, 0);
+extern "C" obj_res lean_elaborator_elaborate_command(b_obj_arg vm_filename, obj_arg vm_cmd, b_obj_arg vm_st) {
+    auto vm_e = cnstr_get(vm_st, 0);
     auto env = to_env(vm_e);
-    auto filename = to_string(vm_filename);
+    auto filename = string_to_std(vm_filename);
     std::stringstream in;
-    auto ngen = to_name_generator(cfield(vm_st, 1));
-    auto vm_lds = cfield(vm_st, 2);
+    auto ngen = to_name_generator(cnstr_get(vm_st, 1));
+    list_ref<object_ref> vm_lds(cnstr_get(vm_st, 2), true);
     local_level_decls lds;
     name_set lvars;
-    while (vm_lds.is_ptr()) {
-        auto it = cfield(vm_lds, 0);
-        auto n = to_name(cfield(it, 0));
-        lds.insert(n, to_level(cfield(it, 1)));
+    for (auto const & vm_ld : vm_lds) {
+        auto n = name(cnstr_get(vm_ld.raw(), 0), true);
+        lds.insert(n, level(cnstr_get(vm_ld.raw(), 1), true));
         // all local decls are variables in Lean 4
         lvars.insert(n);
-        vm_lds = cfield(vm_lds, 1);
     }
-    auto vm_eds = cfield(vm_st, 3);
+    list_ref<object_ref> vm_eds(cnstr_get(vm_st, 3), true);
     local_expr_decls eds;
     name_set vars;
-    while (vm_eds.is_ptr()) {
-        auto it = cfield(vm_eds, 0);
-        auto n = to_name(cfield(it, 0));
-        auto data = cfield(it, 1);
-        eds.insert(n, mk_local(to_name(cfield(data, 0)), n, to_expr(cfield(data, 1)), to_binder_info(cfield(data, 2))));
+    for (auto const & vm_ed : vm_eds) {
+        auto n = name(cnstr_get(vm_ed.raw(), 0), true);
+        auto data = cnstr_get(vm_ed.raw(), 1);
+        eds.insert(n, mk_local(name(cnstr_get(data, 0), true), n, expr(cnstr_get(data, 1), true),
+                               cnstr_get_scalar<binder_info>(data, sizeof(void*) * 2)));
         // all local decls are variables in Lean 4
         vars.insert(n);
-        vm_eds = cfield(vm_eds, 1);
     }
-    auto includes = to_name_set(cfield(vm_st, 4));
-    auto options = to_options(cfield(vm_st, 5));
+    auto includes = to_name_set(cnstr_get(vm_st, 4));
+    auto options = to_options(cnstr_get(vm_st, 5));
 
-    auto cmd = to_expr(vm_cmd);
+    auto cmd = expr(vm_cmd);
     auto pos = get_pos(cmd).value_or(pos_info {1, 0});
     message_log log;
-    vm_obj vm_out = mk_vm_none();
+    obj_arg vm_out = mk_option_none();
     {
         scope_message_log scope3(log);
         io_state ios(options, mk_pretty_formatter_factory());
@@ -709,8 +537,8 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
         parser p(env, ios, in, filename);
         auto s = p.mk_snapshot();
         p.reset(snapshot(p.env(), ngen, lds, eds, lvars, vars, includes, options, true, false,
-                         parser_scope_stack(), to_unsigned(cfield(vm_st, 6)), pos_info{1, 0}));
-        auto ns = to_name(cfield(vm_st, 7));
+                         parser_scope_stack(), nat(cnstr_get(vm_st, 6), true).get_small_value(), pos_info{1, 0}));
+        auto ns = name(cnstr_get(vm_st, 7), true);
         p.set_env(set_namespace(env, ns));
 
         try {
@@ -722,56 +550,77 @@ vm_obj vm_elaborate_command(vm_obj const & vm_filename, vm_obj const & vm_cmd, v
             s->m_lds.for_each([&](name const & n, level const &) {
                 new_lds.insert(s->m_lds.find_idx(n), n);
             });
+            vm_lds = list_ref<object_ref>();
             new_lds.for_each([&](unsigned const &, name const & n) {
-                auto vm_n = to_obj(n);
-                auto vm_ld = mk_vm_constructor(0, vm_n, mk_vm_constructor(4, vm_n));
-                vm_lds = mk_vm_constructor(1, vm_ld, vm_lds);
+                auto vm_ld = mk_cnstr(0, n, mk_cnstr(4, n));
+                vm_lds = cons(vm_ld, vm_lds);
             });
 
+            vm_eds = list_ref<object_ref>();
             for (auto const & ed : s->m_eds.get_entries()) {
                 if (!is_local_p(ed.second)) {
                     // obsolete local ref, ignore
                     continue;
                 }
-                auto vm_ed = mk_vm_constructor(0, to_obj(ed.first), mk_vm_constructor(0,
-                                                                                      to_obj(local_name_p(ed.second)),
-                                                                                      mk_vm_external(new vm_expr(
-                                                                                              local_type_p(ed.second))),
-                                                                                      to_obj(local_info_p(ed.second))));
-                vm_eds = mk_vm_constructor(1, vm_ed, vm_eds);
+                auto vm_sec_var = mk_cnstr(0, local_name_p(ed.second), local_type_p(ed.second), sizeof(binder_info));
+                cnstr_set_scalar(vm_sec_var.raw(), sizeof(void*) * 2, local_info_p(ed.second));
+                auto vm_ed = mk_cnstr(0, ed.first, vm_sec_var);
+                vm_eds = cons(vm_ed, vm_eds);
             }
 
-            auto vm_st2 = mk_vm_constructor(0, {
-                    mk_vm_external(new vm_env(p.env())),
-                    to_obj(s->m_ngen),
-                    vm_lds,
-                    vm_eds,
-                    cfield(vm_st, 4),
-                    cfield(vm_st, 5),
-                    cfield(vm_st, 6),
-                    cfield(vm_st, 7)
-            });
-            vm_out = mk_vm_some(vm_st2);
+            object * args[] = {
+                    to_lean_environment(p.env()),
+                    to_obj(s->m_ngen).steal(),
+                    vm_lds.steal(),
+                    vm_eds.steal(),
+                    cnstr_get(vm_st, 4),
+                    cnstr_get(vm_st, 5),
+                    cnstr_get(vm_st, 6),
+                    cnstr_get(vm_st, 7)
+            };
+            inc(cnstr_get(vm_st, 4));
+            inc(cnstr_get(vm_st, 5));
+            inc(cnstr_get(vm_st, 6));
+            inc(cnstr_get(vm_st, 7));
+            auto vm_st2 = mk_cnstr(0, 8, args);
+            vm_out = mk_option_some(vm_st2.steal());
         } catch (exception & e) {
             message_builder builder(env, ios, filename, pos, message_severity::ERROR);
             builder.set_exception(e);
             builder.report();
         }
     }
-    return mk_vm_constructor(0, vm_out, to_obj(log));
+    return mk_cnstr(0, object_ref(vm_out), log.raw()).steal();
 }
 
-vm_obj vm_expr_local(vm_obj const & vm_pp_name, vm_obj const & vm_name, vm_obj const & vm_type, vm_obj const & vm_binder_info) {
-    return mk_vm_constructor(1, vm_pp_name, vm_name, vm_type, vm_binder_info);
+extern "C" obj_res lean_expr_local(obj_arg vm_name, obj_arg vm_pp_name, obj_arg vm_type, uint8 vm_binder_info) {
+    return mk_local(name(vm_name), name(vm_pp_name), expr(vm_type), static_cast<binder_info>(vm_binder_info)).steal();
+}
+
+static vm_obj vm_lean_expr_local(vm_obj const &, vm_obj const &, vm_obj const &, vm_obj const &) {
+    throw exception("elaborator support has not been implemented in the old VM");
+}
+
+static vm_obj vm_lean_environment_mk_empty() {
+    throw exception("elaborator support has not been implemented in the old VM");
+}
+
+static vm_obj vm_lean_environment_contains(vm_obj const &, vm_obj const &) {
+    throw exception("elaborator support has not been implemented in the old VM");
+}
+
+static vm_obj vm_lean_elaborator_elaborate_command(vm_obj const &, vm_obj const &, vm_obj const &) {
+    throw exception("elaborator support has not been implemented in the old VM");
 }
 
 void initialize_vm_elaborator() {
-    DECLARE_VM_BUILTIN(name({"lean", "expr", "local"}), vm_expr_local);
-    DECLARE_VM_BUILTIN(name({"lean", "environment", "mk_empty"}), vm_environment_mk_empty);
-    DECLARE_VM_BUILTIN(name({"lean", "environment", "contains"}), vm_environment_contains);
-    DECLARE_VM_BUILTIN(name({"lean", "elaborator", "elaborate_command"}), vm_elaborate_command);
+    DECLARE_VM_BUILTIN(name({"lean", "expr", "local"}), vm_lean_expr_local);
+    DECLARE_VM_BUILTIN(name({"lean", "environment", "mk_empty"}), vm_lean_environment_mk_empty);
+    DECLARE_VM_BUILTIN(name({"lean", "environment", "contains"}), vm_lean_environment_contains);
+    DECLARE_VM_BUILTIN(name({"lean", "elaborator", "elaborate_command"}), vm_lean_elaborator_elaborate_command);
 }
 
 void finalize_vm_elaborator() {
+    // del(lean_environment_empty);
 }
 }
diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index bd86865fc8..e611840a97 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -2,4 +2,4 @@ add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
 local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
 init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
-inductive.cpp runtime.cpp)
+inductive.cpp)
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 805ecd22df..919b44c4be 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -111,7 +111,7 @@ public:
     expr(expr const & other):object_ref(other) {}
     expr(expr && other):object_ref(other) {}
     explicit expr(b_obj_arg o, bool b):object_ref(o, b) {}
-    explicit expr(b_obj_arg o):object_ref(o) {}
+    explicit expr(obj_arg o):object_ref(o) {}
     static expr_kind kind(object * o) { return static_cast<expr_kind>(cnstr_tag(o)); }
     expr_kind kind() const { return kind(raw()); }
 
diff --git a/src/kernel/level.h b/src/kernel/level.h
index f7c37f7121..c5ed6d32bf 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -37,12 +37,12 @@ class level : public object_ref {
     friend level mk_imax_core(level const & l1, level const & l2);
     friend level mk_univ_param(name const & n);
     friend level mk_univ_mvar(name const & n);
-    explicit level(b_obj_arg o):object_ref(o) {}
-    explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit level(object_ref && o):object_ref(o) {}
 public:
     /** \brief Universe zero */
     level():object_ref(box(static_cast<unsigned>(level_kind::Zero))) {}
+    explicit level(obj_arg o):object_ref(o) {}
+    explicit level(b_obj_arg o, bool b):object_ref(o, b) {}
     level(level const & other):object_ref(other) {}
     level(level && other):object_ref(other) {}
     level_kind kind() const { return static_cast<level_kind>(obj_tag(raw())); }
diff --git a/src/kernel/runtime.cpp b/src/kernel/runtime.cpp
deleted file mode 100644
index 64c4b23277..0000000000
--- a/src/kernel/runtime.cpp
+++ /dev/null
@@ -1,29 +0,0 @@
-/*
-Copyright (c) 2019 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "runtime/object.h"
-
-namespace lean {
-extern "C" object* lean_expr_local(object*, object*, object*, uint8) {
-    lean_unreachable();
-    return nullptr;
-}
-
-extern "C" object* lean_environment_mk_empty(object*) {
-    lean_unreachable();
-    return nullptr;
-}
-
-extern "C" uint8 lean_environment_contains(object*, object*) {
-    lean_unreachable();
-    return 0;
-}
-
-extern "C" object* lean_elaborator_elaborate_command(object*, object*, object*) {
-    lean_unreachable();
-    return nullptr;
-}
-}
diff --git a/src/library/messages.h b/src/library/messages.h
index 0c4e48fca5..e14a829d67 100644
--- a/src/library/messages.h
+++ b/src/library/messages.h
@@ -88,6 +88,7 @@ public:
     bool has_errors() const;
     void add(message const &);
     buffer<message> to_buffer() const;
+    list_ref<message> & raw() { return m_rev_list; }
 };
 
 struct scope_message_log : flet<message_log *> {
diff --git a/src/runtime/object.h b/src/runtime/object.h
index 5a870a0e20..385b1f63bc 100644
--- a/src/runtime/object.h
+++ b/src/runtime/object.h
@@ -174,6 +174,7 @@ struct task_object : public object {
 /* Base class for wrapping external_object data.
    For example, we use it to wrap the Lean environment object. */
 struct external_object : public object {
+    explicit external_object(object_memory_kind m = c_init_mem_kind): object(object_kind::External, m) {}
     virtual void dealloc() {}
     virtual ~external_object() {}
 };
diff --git a/src/util/list_ref.h b/src/util/list_ref.h
index 9e2a86bcfe..a6a1662c21 100644
--- a/src/util/list_ref.h
+++ b/src/util/list_ref.h
@@ -14,9 +14,10 @@ template<typename T> T const & head(object * o) { return static_cast<T const &>(
 /* Wrapper for manipulating Lean lists in C++ */
 template<typename T>
 class list_ref : public object_ref {
-    list_ref(b_obj_arg o, bool b):object_ref(o, b) {}
 public:
     list_ref():object_ref(box(0)) {}
+    explicit list_ref(obj_arg o):object_ref(o) {}
+    list_ref(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit list_ref(T const & a):object_ref(mk_cnstr(1, a.raw(), box(0))) { inc(a.raw()); }
     explicit list_ref(T const * a) { if (a) *this = list_ref(*a); }
     explicit list_ref(list_ref<T> const * l) { if (l) *this = *l; }
diff --git a/src/util/name.h b/src/util/name.h
index 6be61be8f8..f59c910480 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -61,12 +61,12 @@ public:
     static int cmp_core(object * o1, object * o2);
     size_t size_core(bool unicode) const;
 private:
-    name(b_obj_arg r, bool b):object_ref(r, b) {}
     friend name read_name(deserializer & d);
     explicit name(object_ref && r):object_ref(r) {}
 public:
     name():object_ref(box(static_cast<unsigned>(name_kind::ANONYMOUS))) {}
-    name(obj_arg o):object_ref(o) {}
+    explicit name(obj_arg o):object_ref(o) {}
+    name(b_obj_arg r, bool b):object_ref(r, b) {}
     name(name const & prefix, char const * name);
     name(name const & prefix, unsigned k);
     name(name const & prefix, nat const & n);
diff --git a/src/util/name_generator.h b/src/util/name_generator.h
index ae18e46536..acec5f04de 100644
--- a/src/util/name_generator.h
+++ b/src/util/name_generator.h
@@ -8,7 +8,6 @@ Author: Leonardo de Moura
 #include "util/name.h"
 
 namespace lean {
-class vm_obj;
 /**
    \brief A generator of unique names modulo a prefix.
    If the initial prefix is independent of all other names in the system, then all generated names are unique.
@@ -19,8 +18,8 @@ class name_generator {
     name     m_prefix;
     unsigned m_next_idx;
 
-    friend name_generator to_name_generator(vm_obj const &);
-    friend vm_obj to_obj(name_generator const &);
+    friend name_generator to_name_generator(obj_arg o);
+    friend object_ref to_obj(name_generator const &);
 public:
     name_generator();
     /* Create a name generator with the given prefix.
diff --git a/src/util/nat.h b/src/util/nat.h
index c0ad88e53b..bd078b008a 100644
--- a/src/util/nat.h
+++ b/src/util/nat.h
@@ -11,11 +11,11 @@ Author: Leonardo de Moura
 namespace lean {
 /* Wrapper for manipulating Lean runtime nat values in C++. */
 class nat : public object_ref {
-    nat(b_obj_arg o, bool b):object_ref(o, b) {}
-    explicit nat(obj_arg o):object_ref(o) {}
     static nat wrap(object * o) { return nat(o, true); }
 public:
     nat():object_ref(box(0)) {}
+    explicit nat(obj_arg o):object_ref(o) {}
+    nat(b_obj_arg o, bool b):object_ref(o, b) {}
     explicit nat(int v):object_ref(mk_nat_obj(v < 0 ? 0u : static_cast<unsigned>(v))) {}
     explicit nat(unsigned v):object_ref(mk_nat_obj(v)) {}
     explicit nat(mpz const & v):object_ref(mk_nat_obj(v)) {}