diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index ded166101..f85d48afc 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -30,7 +30,7 @@ io_state * get_io_state(lua_State * L);
 DECL_UDATA(level)
 DEFINE_LUA_LIST(level, push_level, to_level)
 
-int push_optional_level(lua_State * L, optional<level> const & l) {  return l ? push_level(L, *l) : pushnil(L); }
+int push_optional_level(lua_State * L, optional<level> const & l) {  return l ? push_level(L, *l) : push_nil(L); }
 
 static int level_tostring(lua_State * L) {
     std::ostringstream out;
@@ -40,8 +40,8 @@ static int level_tostring(lua_State * L) {
     return 1;
 }
 
-static int level_eq(lua_State * L) { return pushboolean(L, to_level(L, 1) == to_level(L, 2)); }
-static int level_lt(lua_State * L) { return pushboolean(L, is_lt(to_level(L, 1), to_level(L, 2))); }
+static int level_eq(lua_State * L) { return push_boolean(L, to_level(L, 1) == to_level(L, 2)); }
+static int level_lt(lua_State * L) { return push_boolean(L, is_lt(to_level(L, 1), to_level(L, 2))); }
 static int mk_level_zero(lua_State * L) { return push_level(L, mk_level_zero()); }
 static int mk_level_one(lua_State * L)  { return push_level(L, mk_level_one());  }
 static int mk_level_succ(lua_State * L) { return push_level(L, mk_succ(to_level(L, 1))); }
@@ -49,7 +49,7 @@ static int mk_level_max(lua_State * L)  { return push_level(L, mk_max(to_level(L
 static int mk_level_imax(lua_State * L) { return push_level(L, mk_imax(to_level(L, 1), to_level(L, 2))); }
 static int mk_param_univ(lua_State * L) { return push_level(L, mk_param_univ(to_name_ext(L, 1))); }
 static int mk_meta_univ(lua_State * L)  { return push_level(L, mk_meta_univ(to_name_ext(L, 1))); }
-#define LEVEL_PRED(P) static int level_ ## P(lua_State * L) { return pushboolean(L, P(to_level(L, 1))); }
+#define LEVEL_PRED(P) static int level_ ## P(lua_State * L) { return push_boolean(L, P(to_level(L, 1))); }
 LEVEL_PRED(is_zero)
 LEVEL_PRED(is_param)
 LEVEL_PRED(is_meta)
@@ -60,9 +60,9 @@ LEVEL_PRED(is_explicit)
 LEVEL_PRED(has_meta)
 LEVEL_PRED(has_param)
 LEVEL_PRED(is_not_zero)
-static int level_get_kind(lua_State * L) { return pushinteger(L, static_cast<int>(kind(to_level(L, 1)))); }
-static int level_trivially_leq(lua_State * L) { return pushboolean(L, is_trivial(to_level(L, 1), to_level(L, 2))); }
-static int level_is_eqp(lua_State * L) { return pushboolean(L, is_eqp(to_level(L, 1), to_level(L, 2))); }
+static int level_get_kind(lua_State * L) { return push_integer(L, static_cast<int>(kind(to_level(L, 1)))); }
+static int level_trivially_leq(lua_State * L) { return push_boolean(L, is_trivial(to_level(L, 1), to_level(L, 2))); }
+static int level_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_level(L, 1), to_level(L, 2))); }
 
 static int level_id(lua_State * L) {
     level const & l = to_level(L, 1);
@@ -164,8 +164,8 @@ static int mk_binder_info(lua_State * L) {
     else
         return push_expr_binder_info(L, expr_binder_info(lua_toboolean(L, 1), lua_toboolean(L, 2)));
 }
-static int binder_info_is_implicit(lua_State * L) { return pushboolean(L, to_expr_binder_info(L, 1).is_implicit()); }
-static int binder_info_is_cast(lua_State * L) { return pushboolean(L, to_expr_binder_info(L, 1).is_cast()); }
+static int binder_info_is_implicit(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_implicit()); }
+static int binder_info_is_cast(lua_State * L) { return push_boolean(L, to_expr_binder_info(L, 1).is_cast()); }
 static const struct luaL_Reg binder_info_m[] = {
     {"__gc",            expr_binder_info_gc},
     {"is_implicit",     safe_function<binder_info_is_implicit>},
@@ -186,7 +186,7 @@ static void open_binder_info(lua_State * L) {
 DECL_UDATA(expr)
 DEFINE_LUA_LIST(expr, push_expr, to_expr)
 
-int push_optional_expr(lua_State * L, optional<expr> const & e) {  return e ? push_expr(L, *e) : pushnil(L); }
+int push_optional_expr(lua_State * L, optional<expr> const & e) {  return e ? push_expr(L, *e) : push_nil(L); }
 
 expr & to_app(lua_State * L, int idx) {
     expr & r = to_expr(L, idx);
@@ -215,11 +215,11 @@ static int expr_tostring(lua_State * L) {
     options opts    = get_global_options(L);
     environment env = get_global_environment(L);
     out << mk_pair(fmt(env, to_expr(L, 1), opts), opts);
-    return pushstring(L, out.str().c_str());
+    return push_string(L, out.str().c_str());
 }
 
-static int expr_eq(lua_State * L) { return pushboolean(L, to_expr(L, 1) == to_expr(L, 2)); }
-static int expr_lt(lua_State * L) { return pushboolean(L, to_expr(L, 1) < to_expr(L, 2)); }
+static int expr_eq(lua_State * L) { return push_boolean(L, to_expr(L, 1) == to_expr(L, 2)); }
+static int expr_lt(lua_State * L) { return push_boolean(L, to_expr(L, 1) < to_expr(L, 2)); }
 static int expr_mk_constant(lua_State * L) { return push_expr(L, mk_constant(to_name_ext(L, 1))); }
 static int expr_mk_var(lua_State * L) { return push_expr(L, mk_var(luaL_checkinteger(L, 1))); }
 static int expr_mk_app(lua_State * L) {
@@ -309,9 +309,9 @@ static int expr_pi(lua_State * L)  { return expr_abst<Pi, Pi>(L); }
 static int expr_mk_sort(lua_State * L) { return push_expr(L, mk_sort(to_level(L, 1))); }
 static int expr_mk_metavar(lua_State * L) { return push_expr(L, mk_metavar(to_name_ext(L, 1), to_expr(L, 2))); }
 static int expr_mk_local(lua_State * L) { return push_expr(L, mk_local(to_name_ext(L, 1), to_expr(L, 2))); }
-static int expr_get_kind(lua_State * L) { return pushinteger(L, static_cast<int>(to_expr(L, 1).kind())); }
+static int expr_get_kind(lua_State * L) { return push_integer(L, static_cast<int>(to_expr(L, 1).kind())); }
 
-#define EXPR_PRED(P) static int expr_ ## P(lua_State * L) {  return pushboolean(L, P(to_expr(L, 1))); }
+#define EXPR_PRED(P) static int expr_ ## P(lua_State * L) {  return push_boolean(L, P(to_expr(L, 1))); }
 
 EXPR_PRED(is_constant)
 EXPR_PRED(is_var)
@@ -335,7 +335,7 @@ static int expr_fields(lua_State * L) {
     expr & e = to_expr(L, 1);
     switch (e.kind()) {
     case expr_kind::Var:
-        return pushinteger(L, var_idx(e));
+        return push_integer(L, var_idx(e));
     case expr_kind::Constant:
         push_name(L, const_name(e)); push_list_level(L, const_level_params(e)); return 2;
     case expr_kind::Sort:
@@ -380,10 +380,9 @@ static int expr_for_each(lua_State * L) {
 static int expr_has_free_var(lua_State * L) {
     int nargs = lua_gettop(L);
     if (nargs == 2)
-        lua_pushboolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2)));
+        return push_boolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2)));
     else
-        lua_pushboolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3)));
-    return 1;
+        return push_boolean(L, has_free_var(to_expr(L, 1), luaL_checkinteger(L, 2), luaL_checkinteger(L, 3)));
 }
 
 static int expr_lift_free_vars(lua_State * L) {
@@ -441,11 +440,11 @@ static int binder_domain(lua_State * L) { return push_expr(L, binder_domain(to_b
 static int binder_body(lua_State * L) { return push_expr(L, binder_body(to_binder(L, 1))); }
 static int binder_info(lua_State * L) { return push_expr_binder_info(L, binder_info(to_binder(L, 1))); }
 
-static int expr_occurs(lua_State * L) { return pushboolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); }
-static int expr_is_eqp(lua_State * L) { return pushboolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); }
-static int expr_hash(lua_State * L) { return pushinteger(L, to_expr(L, 1).hash()); }
-static int expr_depth(lua_State * L) { return pushinteger(L, get_depth(to_expr(L, 1))); }
-static int expr_is_lt(lua_State * L) { return pushboolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), false)); }
+static int expr_occurs(lua_State * L) { return push_boolean(L, occurs(to_expr(L, 1), to_expr(L, 2))); }
+static int expr_is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_expr(L, 1), to_expr(L, 2))); }
+static int expr_hash(lua_State * L) { return push_integer(L, to_expr(L, 1).hash()); }
+static int expr_depth(lua_State * L) { return push_integer(L, get_depth(to_expr(L, 1))); }
+static int expr_is_lt(lua_State * L) { return push_boolean(L, is_lt(to_expr(L, 1), to_expr(L, 2), false)); }
 
 static int expr_mk_macro(lua_State * L) {
     buffer<expr> args;
@@ -454,8 +453,8 @@ static int expr_mk_macro(lua_State * L) {
 }
 
 static int macro_def(lua_State * L) { return push_macro_definition(L, macro_def(to_macro_app(L, 1))); }
-static int macro_num_args(lua_State * L) { return pushinteger(L, macro_num_args(to_macro_app(L, 1))); }
-static int macro_arg(lua_State * L) { return push_expr(L, macro_arg(to_macro_app(L, 1), pushinteger(L, 2))); }
+static int macro_num_args(lua_State * L) { return push_integer(L, macro_num_args(to_macro_app(L, 1))); }
+static int macro_arg(lua_State * L) { return push_expr(L, macro_arg(to_macro_app(L, 1), push_integer(L, 2))); }
 
 static const struct luaL_Reg expr_m[] = {
     {"__gc",             expr_gc}, // never throws
@@ -559,15 +558,15 @@ static void open_expr(lua_State * L) {
 DECL_UDATA(macro_definition)
 
 int macro_get_name(lua_State * L) { return push_name(L, to_macro_definition(L, 1).get_name()); }
-int macro_trust_level(lua_State * L) { return pushinteger(L, to_macro_definition(L, 1).trust_level()); }
-int macro_eq(lua_State * L) { return pushboolean(L, to_macro_definition(L, 1) == to_macro_definition(L, 2)); }
-int macro_hash(lua_State * L) { return pushinteger(L, to_macro_definition(L, 1).hash()); }
+int macro_trust_level(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).trust_level()); }
+int macro_eq(lua_State * L) { return push_boolean(L, to_macro_definition(L, 1) == to_macro_definition(L, 2)); }
+int macro_hash(lua_State * L) { return push_integer(L, to_macro_definition(L, 1).hash()); }
 static int macro_tostring(lua_State * L) {
     std::ostringstream out;
     formatter fmt   = get_global_formatter(L);
     options opts    = get_global_options(L);
     out << mk_pair(to_macro_definition(L, 1).pp(fmt, opts), opts);
-    return pushstring(L, out.str().c_str());
+    return push_string(L, out.str().c_str());
 }
 
 static const struct luaL_Reg macro_definition_m[] = {
@@ -885,7 +884,7 @@ io_state * get_io_state(lua_State * L) {
 // Justification
 DECL_UDATA(justification)
 
-int push_optional_justification(lua_State * L, optional<justification> const & j) { return j ? push_justification(L, *j) : pushnil(L); }
+int push_optional_justification(lua_State * L, optional<justification> const & j) { return j ? push_justification(L, *j) : push_nil(L); }
 
 static int justification_tostring(lua_State * L) {
     std::ostringstream out;
@@ -895,7 +894,7 @@ static int justification_tostring(lua_State * L) {
     return 1;
 }
 
-#define JST_PRED(P) static int justification_ ## P(lua_State * L) { return pushboolean(L, to_justification(L, 1).P()); }
+#define JST_PRED(P) static int justification_ ## P(lua_State * L) { return push_boolean(L, to_justification(L, 1).P()); }
 JST_PRED(is_none)
 JST_PRED(is_asserted)
 JST_PRED(is_assumption)
@@ -920,7 +919,7 @@ static int justification_pp(lua_State * L) {
 static int justification_assumption_idx(lua_State * L) {
     if (!to_justification(L, 1).is_assumption())
         throw exception("arg #1 must be an assumption justification");
-    return pushinteger(L, assumption_idx(to_justification(L, 1)));
+    return push_integer(L, assumption_idx(to_justification(L, 1)));
 }
 static int justification_child1(lua_State * L) {
     if (!to_justification(L, 1).is_composite())
@@ -932,8 +931,8 @@ static int justification_child2(lua_State * L) {
         throw exception("arg #1 must be a composite justification");
     return push_justification(L, composite_child2(to_justification(L, 1)));
 }
-static int justification_depends_on(lua_State * L) { return pushboolean(L, depends_on(to_justification(L, 1), pushinteger(L, 2))); }
-static int mk_assumption_justification(lua_State * L) { return push_justification(L, mk_assumption_justification(pushinteger(L, 1))); }
+static int justification_depends_on(lua_State * L) { return push_boolean(L, depends_on(to_justification(L, 1), push_integer(L, 2))); }
+static int mk_assumption_justification(lua_State * L) { return push_justification(L, mk_assumption_justification(push_integer(L, 1))); }
 static int mk_justification(lua_State * L) { return push_justification(L, justification()); }
 static int mk_composite1(lua_State * L) { return push_justification(L, mk_composite1(to_justification(L, 1), to_justification(L, 2))); }
 
@@ -1010,21 +1009,21 @@ static int subst_assign(lua_State * L) {
 }
 static int subst_is_assigned(lua_State * L) {
     if (is_expr(L, 2))
-        return pushboolean(L, to_substitution(L, 1).is_assigned(to_expr(L, 2)));
+        return push_boolean(L, to_substitution(L, 1).is_assigned(to_expr(L, 2)));
     else
-        return pushboolean(L, to_substitution(L, 1).is_assigned(to_level(L, 2)));
+        return push_boolean(L, to_substitution(L, 1).is_assigned(to_level(L, 2)));
 }
-static int subst_is_expr_assigned(lua_State * L) { return pushboolean(L, to_substitution(L, 1).is_expr_assigned(to_name_ext(L, 2))); }
-static int subst_is_level_assigned(lua_State * L) { return pushboolean(L, to_substitution(L, 1).is_level_assigned(to_name_ext(L, 2))); }
-static int subst_occurs(lua_State * L) { return pushboolean(L, to_substitution(L, 1).occurs(to_expr(L, 2), to_expr(L, 3))); }
-static int subst_occurs_expr(lua_State * L) { return pushboolean(L, to_substitution(L, 1).occurs_expr(to_name_ext(L, 2), to_expr(L, 3))); }
+static int subst_is_expr_assigned(lua_State * L) { return push_boolean(L, to_substitution(L, 1).is_expr_assigned(to_name_ext(L, 2))); }
+static int subst_is_level_assigned(lua_State * L) { return push_boolean(L, to_substitution(L, 1).is_level_assigned(to_name_ext(L, 2))); }
+static int subst_occurs(lua_State * L) { return push_boolean(L, to_substitution(L, 1).occurs(to_expr(L, 2), to_expr(L, 3))); }
+static int subst_occurs_expr(lua_State * L) { return push_boolean(L, to_substitution(L, 1).occurs_expr(to_name_ext(L, 2), to_expr(L, 3))); }
 static int subst_get_expr_assignment(lua_State * L) {
     auto r = to_substitution(L, 1).get_expr_assignment(to_name_ext(L, 2));
     if (r) {
         push_expr(L, r->first);
         push_justification(L, r->second);
     } else {
-        pushnil(L); pushnil(L);
+        push_nil(L); push_nil(L);
     }
     return 2;
 }
@@ -1034,7 +1033,7 @@ static int subst_get_level_assignment(lua_State * L) {
         push_level(L, r->first);
         push_justification(L, r->second);
     } else {
-        pushnil(L); pushnil(L);
+        push_nil(L); push_nil(L);
     }
     return 2;
 }
@@ -1045,7 +1044,7 @@ static int subst_get_assignment(lua_State * L) {
             push_expr(L, r->first);
             push_justification(L, r->second);
         } else {
-            pushnil(L); pushnil(L);
+            push_nil(L); push_nil(L);
         }
     } else {
         auto r = to_substitution(L, 1).get_assignment(to_level(L, 2));
@@ -1053,7 +1052,7 @@ static int subst_get_assignment(lua_State * L) {
             push_level(L, r->first);
             push_justification(L, r->second);
         } else {
-            pushnil(L); pushnil(L);
+            push_nil(L); push_nil(L);
         }
     }
     return 2;
@@ -1111,361 +1110,3 @@ void open_kernel_module(lua_State * L) {
     open_substitution(L);
 }
 }
-
-#if 0
-namespace lean {
-
-DECL_UDATA(object)
-
-int push_optional_object(lua_State * L, optional<object> const & o) {
-    if (o)
-        push_object(L, *o);
-    else
-        lua_pushnil(L);
-    return 1;
-}
-
-static int object_keyword(lua_State * L) {
-    lua_pushstring(L, to_object(L, 1).keyword());
-    return 1;
-}
-
-static int object_has_name(lua_State * L) {
-    lua_pushboolean(L, to_object(L, 1).has_name());
-    return 1;
-}
-
-static int object_get_name(lua_State * L) {
-    object const & o = to_object(L, 1);
-    if (!o.has_name())
-        throw exception("kernel object does not have a name");
-    return push_name(L, o.get_name());
-}
-
-static int object_has_type(lua_State * L) {
-    lua_pushboolean(L, to_object(L, 1).has_type());
-    return 1;
-}
-
-static int object_get_type(lua_State * L) {
-    object const & o = to_object(L, 1);
-    if (!o.has_type())
-        throw exception("kernel object does not have a type");
-    return push_expr(L, o.get_type());
-}
-
-static int object_has_cnstr_level(lua_State * L) {
-    lua_pushboolean(L, to_object(L, 1).has_cnstr_level());
-    return 1;
-}
-
-static int object_get_cnstr_level(lua_State * L) {
-    object const & o = to_object(L, 1);
-    if (!o.has_cnstr_level())
-        throw exception("kernel object does not have a constraint level");
-    return push_level(L, o.get_cnstr_level());
-}
-
-static int object_get_value(lua_State * L) {
-    object const & o = to_object(L, 1);
-    if (!o.is_definition() && !o.is_builtin())
-        throw exception("kernel object is not a definition/theorem/builtin");
-    return push_expr(L, o.get_value());
-}
-
-static int object_get_weight(lua_State * L) {
-    object const & o = to_object(L, 1);
-    if (!o.is_definition())
-        throw exception("kernel object is not a definition");
-    lua_pushinteger(L, o.get_weight());
-    return 1;
-}
-
-#define OBJECT_PRED(P)                                  \
-static int object_ ## P(lua_State * L) {                \
-    lua_pushboolean(L, to_object(L, 1).P());    \
-    return 1;                                           \
-}
-
-OBJECT_PRED(is_definition)
-OBJECT_PRED(is_opaque)
-OBJECT_PRED(is_axiom)
-OBJECT_PRED(is_theorem)
-OBJECT_PRED(is_var_decl)
-OBJECT_PRED(is_builtin)
-OBJECT_PRED(is_builtin_set)
-
-#define OBJECT_EXTRA_PRED(P)                    \
-static int object_ ## P(lua_State * L) {        \
-    lua_pushboolean(L, P(to_object(L, 1)));     \
-    return 1;                                   \
-}
-
-OBJECT_EXTRA_PRED(is_begin_import)
-OBJECT_EXTRA_PRED(is_begin_builtin_import)
-OBJECT_EXTRA_PRED(is_end_import)
-
-static int object_in_builtin_set(lua_State * L) {
-    lua_pushboolean(L, to_object(L, 1).in_builtin_set(to_expr(L, 2)));
-    return 1;
-}
-
-static int object_tostring(lua_State * L) {
-    std::ostringstream out;
-    formatter fmt = get_global_formatter(L);
-    options opts  = get_global_options(L);
-    out << mk_pair(fmt(to_object(L, 1), opts), opts);
-    lua_pushstring(L, out.str().c_str());
-    return 1;
-}
-
-static const struct luaL_Reg object_m[] = {
-    {"__gc",            object_gc}, // never throws
-    {"__tostring",      safe_function<object_tostring>},
-    {"keyword",         safe_function<object_keyword>},
-    {"has_name",        safe_function<object_has_name>},
-    {"get_name",        safe_function<object_get_name>},
-    {"has_type",        safe_function<object_has_type>},
-    {"get_type",        safe_function<object_get_type>},
-    {"has_cnstr_level", safe_function<object_has_cnstr_level>},
-    {"get_cnstr_level", safe_function<object_get_cnstr_level>},
-    {"is_definition",   safe_function<object_is_definition>},
-    {"is_opaque",       safe_function<object_is_opaque>},
-    {"get_value",       safe_function<object_get_value>},
-    {"get_weight",      safe_function<object_get_weight>},
-    {"is_axiom",        safe_function<object_is_axiom>},
-    {"is_theorem",      safe_function<object_is_theorem>},
-    {"is_var_decl",     safe_function<object_is_var_decl>},
-    {"is_builtin",      safe_function<object_is_builtin>},
-    {"is_builtin_set",  safe_function<object_is_builtin_set>},
-    {"in_builtin_set",  safe_function<object_in_builtin_set>},
-    {"is_begin_import", safe_function<object_is_begin_import>},
-    {"is_begin_builtin_import", safe_function<object_is_begin_builtin_import>},
-    {"is_end_import",   safe_function<object_is_end_import>},
-    {0, 0}
-};
-
-static void open_object(lua_State * L) {
-    luaL_newmetatable(L, object_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, object_m, 0);
-
-    SET_GLOBAL_FUN(object_pred, "is_kernel_object");
-}
-
-
-DECL_UDATA(metavar_env)
-
-static int menv_mk_metavar(lua_State * L) {
-    int nargs = lua_gettop(L);
-    if (nargs == 1) {
-        return push_expr(L, to_metavar_env(L, 1)->mk_metavar());
-    } else if (nargs == 2) {
-        return push_expr(L, to_metavar_env(L, 1)->mk_metavar(to_context(L, 2)));
-    } else {
-        return push_expr(L, to_metavar_env(L, 1)->mk_metavar(to_context(L, 2), some_expr(to_expr(L, 3))));
-    }
-}
-
-static expr & to_metavar(lua_State * L, int i, bool lctx = true) {
-    expr & e = to_expr(L, i);
-    if (is_metavar(e)) {
-        if (lctx || !has_local_context(e))
-            return e;
-        throw exception(sstream() << "arg #" << i << " must be a metavariable without a local context");
-    }
-    throw exception(sstream() << "arg #" << i << " must be a metavariable");
-}
-
-static int menv_get_timestamp(lua_State * L) {
-    lua_pushinteger(L, to_metavar_env(L, 1)->get_timestamp());
-    return 1;
-}
-
-static int menv_get_context(lua_State * L) {
-    if (is_expr(L, 2))
-        return push_context(L, to_metavar_env(L, 1)->get_context(to_metavar(L, 2, false)));
-    else
-        return push_context(L, to_metavar_env(L, 1)->get_context(to_name_ext(L, 2)));
-}
-
-static int menv_has_type(lua_State * L) {
-    if (is_expr(L, 2))
-        lua_pushboolean(L, to_metavar_env(L, 1)->has_type(to_metavar(L, 2)));
-    else
-        lua_pushboolean(L, to_metavar_env(L, 1)->has_type(to_name_ext(L, 2)));
-    return 1;
-}
-
-static int menv_get_type(lua_State * L) {
-    if (is_expr(L, 2))
-        return push_expr(L, to_metavar_env(L, 1)->get_type(to_metavar(L, 2)));
-    else
-        return push_expr(L, to_metavar_env(L, 1)->get_type(to_name_ext(L, 2)));
-}
-
-static int menv_is_assigned(lua_State * L) {
-    if (is_expr(L, 2))
-        lua_pushboolean(L, to_metavar_env(L, 1)->is_assigned(to_metavar(L, 2)));
-    else
-        lua_pushboolean(L, to_metavar_env(L, 1)->is_assigned(to_name_ext(L, 2)));
-    return 1;
-}
-
-static int menv_assign(lua_State * L) {
-    int nargs = lua_gettop(L);
-    justification jst;
-    if (nargs == 4)
-        jst = to_justification(L, 4);
-    if (is_expr(L, 2))
-        to_metavar_env(L, 1)->assign(to_metavar(L, 2, false), to_expr(L, 3), jst);
-    else
-        to_metavar_env(L, 1)->assign(to_name_ext(L, 2), to_expr(L, 3), jst);
-    return 0;
-}
-
-static int menv_get_subst(lua_State * L) {
-    if (is_expr(L, 2))
-        return push_optional_expr(L, to_metavar_env(L, 1)->get_subst(to_metavar(L, 2)));
-    else
-        return push_optional_expr(L, to_metavar_env(L, 1)->get_subst(to_name_ext(L, 2)));
-}
-
-static int menv_get_justification(lua_State * L) {
-    if (is_expr(L, 2))
-        return push_optional_justification(L, to_metavar_env(L, 1)->get_justification(to_metavar(L, 2)));
-    else
-        return push_optional_justification(L, to_metavar_env(L, 1)->get_justification(to_name_ext(L, 2)));
-}
-
-static int menv_get_subst_jst(lua_State * L) {
-    optional<std::pair<expr, justification>> r;
-    if (is_expr(L, 2)) {
-        r = to_metavar_env(L, 1)->get_subst_jst(to_metavar(L, 2));
-    } else {
-        r = to_metavar_env(L, 1)->get_subst_jst(to_name_ext(L, 2));
-    }
-    if (r) {
-        push_expr(L, r->first);
-        push_justification(L, r->second);
-        return 2;
-    } else {
-        return 0;
-    }
-}
-
-static int menv_for_each_subst(lua_State * L) {
-    luaL_checktype(L, 2, LUA_TFUNCTION); // user-fun
-    to_metavar_env(L, 1)->for_each_subst([&](name const & n, expr const & e) {
-            lua_pushvalue(L, 2); // push user-fun
-            push_name(L, n);
-            push_expr(L, e);
-            pcall(L, 2, 0, 0);
-        });
-    return 0;
-}
-
-static int mk_metavar_env(lua_State * L) {
-    if (lua_gettop(L) == 1)
-        return push_metavar_env(L, metavar_env(to_name_ext(L, 1)));
-    else
-        return push_metavar_env(L, metavar_env());
-}
-
-static int menv_copy(lua_State * L) {
-    return push_metavar_env(L, metavar_env(to_metavar_env(L, 1).copy()));
-}
-
-static int instantiate_metavars(lua_State * L) {
-    return push_expr(L, to_metavar_env(L, 2)->instantiate_metavars(to_expr(L, 1)));
-}
-
-static const struct luaL_Reg metavar_env_m[] = {
-    {"__gc",              metavar_env_gc}, // never throws
-    {"mk_metavar",        safe_function<menv_mk_metavar>},
-    {"get_timestamp",     safe_function<menv_get_timestamp>},
-    {"get_context",       safe_function<menv_get_context>},
-    {"has_type",          safe_function<menv_has_type>},
-    {"get_type",          safe_function<menv_get_type>},
-    {"is_assigned",       safe_function<menv_is_assigned>},
-    {"assign",            safe_function<menv_assign>},
-    {"get_subst",         safe_function<menv_get_subst>},
-    {"get_justification", safe_function<menv_get_justification>},
-    {"get_subst_jst",     safe_function<menv_get_subst_jst>},
-    {"for_each_subst",    safe_function<menv_for_each_subst>},
-    {"copy",              safe_function<menv_copy>},
-    {0, 0}
-};
-
-static void open_metavar_env(lua_State * L) {
-    luaL_newmetatable(L, metavar_env_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, metavar_env_m, 0);
-
-    SET_GLOBAL_FUN(mk_metavar_env,   "metavar_env");
-    SET_GLOBAL_FUN(metavar_env_pred, "is_metavar_env");
-    SET_GLOBAL_FUN(instantiate_metavars, "instantiate_metavars");
-}
-
-constexpr char const * type_inferer_mt = "type_inferer";
-type_inferer & to_type_inferer(lua_State * L, int i) { return *static_cast<type_inferer*>(luaL_checkudata(L, i, type_inferer_mt)); }
-DECL_PRED(type_inferer)
-DECL_GC(type_inferer)
-
-static int type_inferer_call(lua_State * L) {
-    int nargs = lua_gettop(L);
-    type_inferer & inferer = to_type_inferer(L, 1);
-    if (nargs == 2)
-        return push_expr(L, inferer(to_expr(L, 2)));
-    else
-        return push_expr(L, inferer(to_expr(L, 2), to_context(L, 3)));
-}
-
-static int type_inferer_clear(lua_State * L) {
-    to_type_inferer(L, 1).clear();
-    return 0;
-}
-
-static int mk_type_inferer(lua_State * L) {
-    void * mem = lua_newuserdata(L, sizeof(type_inferer));
-    new (mem) type_inferer(to_environment(L, 1));
-    luaL_getmetatable(L, type_inferer_mt);
-    lua_setmetatable(L, -2);
-    return 1;
-}
-
-static const struct luaL_Reg type_inferer_m[] = {
-    {"__gc",            type_inferer_gc}, // never throws
-    {"__call",          safe_function<type_inferer_call>},
-    {"clear",           safe_function<type_inferer_clear>},
-    {0, 0}
-};
-
-void open_type_inferer(lua_State * L) {
-    luaL_newmetatable(L, type_inferer_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, type_inferer_m, 0);
-
-    SET_GLOBAL_FUN(mk_type_inferer,          "type_inferer");
-    SET_GLOBAL_FUN(type_inferer_pred,        "is_type_inferer");
-}
-
-
-void open_kernel_module(lua_State * L) {
-    open_level(L);
-    open_local_context(L);
-    open_expr(L);
-    open_context(L);
-    open_formatter(L);
-    open_environment(L);
-    open_object(L);
-    open_justification(L);
-    open_metavar_env(L);
-    open_type_inferer(L);
-    open_io_state(L);
-}
-}
-#endif
diff --git a/src/util/exception.cpp b/src/util/exception.cpp
index b9f5791de..6b6ae5139 100644
--- a/src/util/exception.cpp
+++ b/src/util/exception.cpp
@@ -69,7 +69,7 @@ bool is_exception(lua_State * L, int i) {
 }
 
 static int exception_what(lua_State * L) {
-    return pushstring(L, to_exception(L, 1).what());
+    return push_string(L, to_exception(L, 1).what());
 }
 
 static int exception_rethrow(lua_State * L) {
@@ -78,7 +78,7 @@ static int exception_rethrow(lua_State * L) {
 }
 
 static int exception_pred(lua_State * L) {
-    return pushboolean(L, is_exception(L, 1));
+    return push_boolean(L, is_exception(L, 1));
 }
 
 static const struct luaL_Reg exception_m[] = {
diff --git a/src/util/list_lua.h b/src/util/list_lua.h
index 3d1a02584..960fdd35e 100644
--- a/src/util/list_lua.h
+++ b/src/util/list_lua.h
@@ -34,7 +34,7 @@ static int list_ ## T ## _mk(lua_State * L) {                           \
     int nargs = lua_gettop(L);                                          \
     return (nargs == 0) ? list_ ## T ## _nil(L) : list_ ## T ## _cons(L); \
 }                                                                       \
-static int list_ ## T ## _is_nil(lua_State * L) { return pushboolean(L, is_nil(to_list_ ## T(L, 1))); } \
+static int list_ ## T ## _is_nil(lua_State * L) { return push_boolean(L, is_nil(to_list_ ## T(L, 1))); } \
 static int list_ ## T ## _car(lua_State * L) {                          \
     list<T> & l = to_list_ ## T(L, 1);                                  \
     if (is_nil(l)) throw exception("arg #1 must be a cons cell");       \
@@ -45,8 +45,8 @@ static int list_ ## T ## _cdr(lua_State * L) {                          \
     if (is_nil(l)) throw exception("arg #1 must be a cons cell");       \
     return push_list_ ## T(L, cdr(l));                                  \
 }                                                                       \
-static int list_ ## T ## _eq(lua_State * L) { return pushboolean(L, to_list_ ## T(L, 1) == to_list_ ## T(L, 2)); } \
-static int list_ ## T ## _is_eqp(lua_State * L) { return pushboolean(L, is_eqp(to_list_ ## T(L, 1), to_list_ ## T(L, 2))); } \
+static int list_ ## T ## _eq(lua_State * L) { return push_boolean(L, to_list_ ## T(L, 1) == to_list_ ## T(L, 2)); } \
+static int list_ ## T ## _is_eqp(lua_State * L) { return push_boolean(L, is_eqp(to_list_ ## T(L, 1), to_list_ ## T(L, 2))); } \
 static const struct luaL_Reg list_ ## T ## _m[] = {                     \
     {"__gc",            list_ ## T ## _gc},                             \
     {"__eq",            safe_function<list_ ## T ## _eq>},              \
diff --git a/src/util/lua.h b/src/util/lua.h
index 32d950a73..7ad5cdd09 100644
--- a/src/util/lua.h
+++ b/src/util/lua.h
@@ -132,11 +132,11 @@ lua_migrate_fn get_migrate_fn(lua_State * src, int i);
 
 // =======================================
 // Useful macros
-inline int pushboolean(lua_State * L, bool b) { lua_pushboolean(L, b); return 1; }
-inline int pushstring(lua_State * L, char const * s) { lua_pushstring(L, s); return 1; }
-inline int pushinteger(lua_State * L, lua_Integer v) { lua_pushinteger(L, v); return 1; }
-inline int pushnumber(lua_State * L, lua_Number v) { lua_pushnumber(L, v); return 1; }
-inline int pushnil(lua_State * L) { lua_pushnil(L); return 1; }
+inline int push_boolean(lua_State * L, bool b) { lua_pushboolean(L, b); return 1; }
+inline int push_string(lua_State * L, char const * s) { lua_pushstring(L, s); return 1; }
+inline int push_integer(lua_State * L, lua_Integer v) { lua_pushinteger(L, v); return 1; }
+inline int push_number(lua_State * L, lua_Number v) { lua_pushnumber(L, v); return 1; }
+inline int push_nil(lua_State * L) { lua_pushnil(L); return 1; }
 // =======================================
 
 }
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 089f36a8a..dc3236a33 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -473,11 +473,11 @@ name to_name_ext(lua_State * L, int idx) {
     }
 }
 
-static int name_tostring(lua_State * L) { return pushstring(L, to_name(L, 1).to_string().c_str()); }
-static int name_eq(lua_State * L) { return pushboolean(L, to_name(L, 1) == to_name(L, 2)); }
-static int name_lt(lua_State * L) { return pushboolean(L, to_name(L, 1) < to_name(L, 2)); }
-static int name_hash(lua_State * L) { return pushinteger(L, to_name(L, 1).hash()); }
-#define NAME_PRED(P) static int name_ ## P(lua_State * L) { return pushboolean(L, to_name(L, 1).P()); }
+static int name_tostring(lua_State * L) { return push_string(L, to_name(L, 1).to_string().c_str()); }
+static int name_eq(lua_State * L) { return push_boolean(L, to_name(L, 1) == to_name(L, 2)); }
+static int name_lt(lua_State * L) { return push_boolean(L, to_name(L, 1) < to_name(L, 2)); }
+static int name_hash(lua_State * L) { return push_integer(L, to_name(L, 1).hash()); }
+#define NAME_PRED(P) static int name_ ## P(lua_State * L) { return push_boolean(L, to_name(L, 1).P()); }
 NAME_PRED(is_atomic)
 NAME_PRED(is_anonymous)
 NAME_PRED(is_string)
@@ -492,13 +492,13 @@ static int name_get_prefix(lua_State * L) {
 static int name_get_numeral(lua_State * L) {
     if (!to_name(L, 1).is_numeral())
         throw exception("invalid get_numeral, hierarchical name with numeric head expected");
-    return pushinteger(L, to_name(L, 1).get_numeral());
+    return push_integer(L, to_name(L, 1).get_numeral());
 }
 
 static int name_get_string(lua_State * L) {
     if (!to_name(L, 1).is_string())
         throw exception("invalid get_string,  hierarchical name with string head expected");
-    return pushstring(L, to_name(L, 1).get_string());
+    return push_string(L, to_name(L, 1).get_string());
 }
 
 static const struct luaL_Reg name_m[] = {
diff --git a/src/util/numerics/mpq.cpp b/src/util/numerics/mpq.cpp
index 52d008421..7c309d1c1 100644
--- a/src/util/numerics/mpq.cpp
+++ b/src/util/numerics/mpq.cpp
@@ -173,15 +173,15 @@ static int mpq_tostring(lua_State * L) {
     mpq * n = static_cast<mpq*>(luaL_checkudata(L, 1, mpq_mt));
     std::ostringstream out;
     out << *n;
-    return pushstring(L, out.str().c_str());
+    return push_string(L, out.str().c_str());
 }
 
 static int mpq_eq(lua_State * L) {
-    return pushboolean(L, to_mpq<1>(L) == to_mpq<2>(L));
+    return push_boolean(L, to_mpq<1>(L) == to_mpq<2>(L));
 }
 
 static int mpq_lt(lua_State * L) {
-    return pushboolean(L, to_mpq<1>(L) < to_mpq<2>(L));
+    return push_boolean(L, to_mpq<1>(L) < to_mpq<2>(L));
 }
 
 static int mpq_add(lua_State * L) {
diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp
index 6d473a414..3c695c4ff 100644
--- a/src/util/numerics/mpz.cpp
+++ b/src/util/numerics/mpz.cpp
@@ -121,15 +121,15 @@ static int mpz_tostring(lua_State * L) {
     mpz * n = static_cast<mpz*>(luaL_checkudata(L, 1, mpz_mt));
     std::ostringstream out;
     out << *n;
-    return pushstring(L, out.str().c_str());
+    return push_string(L, out.str().c_str());
 }
 
 static int mpz_eq(lua_State * L) {
-    return pushboolean(L, to_mpz<1>(L) == to_mpz<2>(L));
+    return push_boolean(L, to_mpz<1>(L) == to_mpz<2>(L));
 }
 
 static int mpz_lt(lua_State * L) {
-    return pushboolean(L, to_mpz<1>(L) < to_mpz<2>(L));
+    return push_boolean(L, to_mpz<1>(L) < to_mpz<2>(L));
 }
 
 static int mpz_add(lua_State * L) {
diff --git a/src/util/rb_map.cpp b/src/util/rb_map.cpp
index 1bad9d291..db35fa00a 100644
--- a/src/util/rb_map.cpp
+++ b/src/util/rb_map.cpp
@@ -18,15 +18,15 @@ static int mk_lua_rb_map(lua_State * L) {
 }
 
 static int lua_rb_map_size(lua_State * L) {
-    return pushinteger(L, to_lua_rb_map(L, 1).size());
+    return push_integer(L, to_lua_rb_map(L, 1).size());
 }
 
 static int lua_rb_map_contains(lua_State * L) {
-    return pushboolean(L, to_lua_rb_map(L, 1).contains(luaref(L, 2)));
+    return push_boolean(L, to_lua_rb_map(L, 1).contains(luaref(L, 2)));
 }
 
 static int lua_rb_map_empty(lua_State * L) {
-    return pushboolean(L, to_lua_rb_map(L, 1).empty());
+    return push_boolean(L, to_lua_rb_map(L, 1).empty());
 }
 
 static int lua_rb_map_insert(lua_State * L) {
diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp
index 31fa91094..b29391f6f 100644
--- a/src/util/script_state.cpp
+++ b/src/util/script_state.cpp
@@ -298,7 +298,7 @@ int state_set_global(lua_State * L) {
 }
 
 static int state_pred(lua_State * L) {
-    return pushboolean(L, is_state(L, 1));
+    return push_boolean(L, is_state(L, 1));
 }
 
 static const struct luaL_Reg state_m[] = {
@@ -537,7 +537,7 @@ static int thread_gc(lua_State * L) {
 }
 
 static int thread_pred(lua_State * L) {
-    return pushboolean(L, is_thread(L, 1));
+    return push_boolean(L, is_thread(L, 1));
 }
 
 static int thread_write(lua_State * L) {
diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp
index 095a3788a..97da3bb71 100644
--- a/src/util/sexpr/format.cpp
+++ b/src/util/sexpr/format.cpp
@@ -416,7 +416,7 @@ format to_format_elem(lua_State * L, int idx) {
 static int format_tostring(lua_State * L) {
     std::ostringstream out;
     out << mk_pair(to_format(L, 1), get_global_options(L));
-    return pushstring(L, out.str().c_str());
+    return push_string(L, out.str().c_str());
 }
 
 static int format_concat(lua_State * L) {
diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp
index 8d94b28ed..c273c0064 100644
--- a/src/util/sexpr/options.cpp
+++ b/src/util/sexpr/options.cpp
@@ -231,49 +231,49 @@ static int mk_options(lua_State * L) {
 static int options_tostring(lua_State * L) {
     std::ostringstream out;
     out << to_options(L, 1);
-    return pushstring(L, out.str().c_str());
+    return push_string(L, out.str().c_str());
 }
 
 static int options_size(lua_State * L) {
-    return pushinteger(L, to_options(L, 1).size());
+    return push_integer(L, to_options(L, 1).size());
 }
 
 static int options_contains(lua_State * L) {
-    return pushboolean(L, to_options(L, 1).contains(to_name_ext(L, 2)));
+    return push_boolean(L, to_options(L, 1).contains(to_name_ext(L, 2)));
 }
 
 static int options_empty(lua_State * L) {
-    return pushboolean(L, to_options(L, 1).empty());
+    return push_boolean(L, to_options(L, 1).empty());
 }
 
 static int options_get_bool(lua_State * L) {
     int nargs = lua_gettop(L);
     bool defval = nargs < 3 ? false : lua_toboolean(L, 3);
-    return pushboolean(L, to_options(L, 1).get_bool(to_name_ext(L, 2), defval));
+    return push_boolean(L, to_options(L, 1).get_bool(to_name_ext(L, 2), defval));
 }
 
 static int options_get_int(lua_State * L) {
     int nargs = lua_gettop(L);
     int defval = nargs < 3 ? 0 : lua_tointeger(L, 3);
-    return pushinteger(L, to_options(L, 1).get_int(to_name_ext(L, 2), defval));
+    return push_integer(L, to_options(L, 1).get_int(to_name_ext(L, 2), defval));
 }
 
 static int options_get_unsigned(lua_State * L) {
     int nargs = lua_gettop(L);
     unsigned defval = nargs < 3 ? 0 : lua_tointeger(L, 3);
-    return pushnumber(L, to_options(L, 1).get_unsigned(to_name_ext(L, 2), defval));
+    return push_number(L, to_options(L, 1).get_unsigned(to_name_ext(L, 2), defval));
 }
 
 static int options_get_double(lua_State * L) {
     int nargs = lua_gettop(L);
     double defval = nargs < 3 ? 0.0 : lua_tonumber(L, 3);
-    return pushnumber(L, to_options(L, 1).get_double(to_name_ext(L, 2), defval));
+    return push_number(L, to_options(L, 1).get_double(to_name_ext(L, 2), defval));
 }
 
 static int options_get_string(lua_State * L) {
     int nargs = lua_gettop(L);
     char const * defval = nargs < 3 ? "" : lua_tostring(L, 3);
-    return pushstring(L, to_options(L, 1).get_string(to_name_ext(L, 2), defval));
+    return push_string(L, to_options(L, 1).get_string(to_name_ext(L, 2), defval));
 }
 
 static int options_update_bool(lua_State * L) {
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 09d83ea51..d906481b2 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -365,7 +365,7 @@ DECL_UDATA(sexpr)
 static int sexpr_tostring(lua_State * L) {
     std::ostringstream out;
     out << to_sexpr(L, 1);
-    return pushstring(L, out.str().c_str());
+    return push_string(L, out.str().c_str());
 }
 
 static sexpr to_sexpr_elem(lua_State * L, int idx) {
@@ -405,10 +405,10 @@ static int mk_sexpr(lua_State * L) {
     return push_sexpr(L, r);
 }
 
-static int sexpr_eq(lua_State * L)        { return pushboolean(L, to_sexpr(L, 1) == to_sexpr(L, 2)); }
-static int sexpr_lt(lua_State * L)        { return pushboolean(L, to_sexpr(L, 1) < to_sexpr(L, 2)); }
+static int sexpr_eq(lua_State * L)        { return push_boolean(L, to_sexpr(L, 1) == to_sexpr(L, 2)); }
+static int sexpr_lt(lua_State * L)        { return push_boolean(L, to_sexpr(L, 1) < to_sexpr(L, 2)); }
 
-#define SEXPR_PRED(P) static int sexpr_ ## P(lua_State * L) { return pushboolean(L, P(to_sexpr(L, 1))); }
+#define SEXPR_PRED(P) static int sexpr_ ## P(lua_State * L) { return push_boolean(L, P(to_sexpr(L, 1))); }
 
 SEXPR_PRED(is_nil)
 SEXPR_PRED(is_cons)
@@ -426,7 +426,7 @@ static int sexpr_length(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_list(e))
         throw exception("s-expression is not a list");
-    return pushinteger(L, length(e));
+    return push_integer(L, length(e));
 }
 
 static int sexpr_head(lua_State * L) {
@@ -447,28 +447,28 @@ static int sexpr_to_bool(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_bool(e))
         throw exception("s-expression is not a Boolean");
-    return pushboolean(L, to_bool(e));
+    return push_boolean(L, to_bool(e));
 }
 
 static int sexpr_to_string(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_string(e))
         throw exception("s-expression is not a string");
-    return pushstring(L, to_string(e).c_str());
+    return push_string(L, to_string(e).c_str());
 }
 
 static int sexpr_to_int(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_int(e))
         throw exception("s-expression is not an integer");
-    return pushinteger(L, to_int(e));
+    return push_integer(L, to_int(e));
 }
 
 static int sexpr_to_double(lua_State * L) {
     sexpr const & e = to_sexpr(L, 1);
     if (!is_double(e))
         throw exception("s-expression is not a double");
-    return pushnumber(L, to_double(e));
+    return push_number(L, to_double(e));
 }
 
 static int sexpr_to_name(lua_State * L) {
@@ -493,7 +493,7 @@ static int sexpr_to_mpq(lua_State * L) {
 }
 
 static int sexpr_get_kind(lua_State * L) {
-    return pushinteger(L, static_cast<int>(to_sexpr(L, 1).kind()));
+    return push_integer(L, static_cast<int>(to_sexpr(L, 1).kind()));
 }
 
 static int sexpr_fields(lua_State * L) {