diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 63b2950ed..30efa3e40 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -225,8 +225,8 @@ set(LEAN_LIBS ${LEAN_LIBS} library)
 # set(LEAN_LIBS ${LEAN_LIBS} elaborator)
 # add_subdirectory(library/tactic)
 # set(LEAN_LIBS ${LEAN_LIBS} tactic)
-# add_subdirectory(library/error_handling)
-# set(LEAN_LIBS ${LEAN_LIBS} error_handling)
+add_subdirectory(library/error_handling)
+set(LEAN_LIBS ${LEAN_LIBS} error_handling)
 # add_subdirectory(frontends/lean)
 # set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 add_subdirectory(frontends/lua)
diff --git a/src/frontends/lua/register_modules.cpp b/src/frontends/lua/register_modules.cpp
index 26f00c822..111b0df3c 100644
--- a/src/frontends/lua/register_modules.cpp
+++ b/src/frontends/lua/register_modules.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include "util/script_state.h"
 #include "util/numerics/register_module.h"
 #include "util/sexpr/register_module.h"
-// #include "library/register_module.h"
+#include "library/register_module.h"
 // #include "library/io_state_stream.h"
 // #include "library/arith/register_module.h"
 // #include "library/simplifier/register_module.h"
@@ -18,7 +18,7 @@ namespace lean {
 void register_modules() {
     register_numerics_module();
     register_sexpr_module();
-    // register_core_module();
+    register_core_module();
     // register_arith_module();
     // register_simplifier_module();
     // register_tactic_module();
diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 6cffde8b2..cad233401 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -1,7 +1,5 @@
 add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp
-  occurs.cpp)
-# io_state_stream.cpp
-# kernel_bindings.cpp
+  occurs.cpp kernel_bindings.cpp io_state_stream.cpp)
 # context_to_lambda.cpp placeholder.cpp
 # fo_unify.cpp bin_op.cpp equality.cpp
 # hop_match.cpp)
diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp
index 705235631..01dbe9e1e 100644
--- a/src/library/error_handling/error_handling.cpp
+++ b/src/library/error_handling/error_handling.cpp
@@ -11,10 +11,10 @@ Author: Leonardo de Moura
 #include "kernel/kernel_exception.h"
 #include "kernel/for_each_fn.h"
 #include "library/io_state_stream.h"
-#include "library/elaborator/elaborator_justification.h"
-#include "library/elaborator/elaborator_exception.h"
+// #include "library/elaborator/elaborator_justification.h"
+// #include "library/elaborator/elaborator_exception.h"
 #include "library/parser_nested_exception.h"
-#include "library/unsolved_metavar_exception.h"
+// #include "library/unsolved_metavar_exception.h"
 
 namespace lean {
 void display_error_pos(io_state const & ios, char const * strm_name, unsigned line, unsigned pos) {
@@ -51,29 +51,30 @@ static void display_error(io_state const & ios, pos_info_provider const * p, ker
     regular(ios) << " " << ex << endl;
 }
 
-static void display_error(io_state const & ios, pos_info_provider const * p, elaborator_exception const & ex) {
-    formatter fmt = ios.get_formatter();
-    options opts  = ios.get_options();
-    auto j = ex.get_justification();
-    j = remove_detail(j);
-    regular(ios) << mk_pair(j.pp(fmt, opts, p, true), opts) << endl;
-}
+// static void display_error(io_state const & ios, pos_info_provider const * p, elaborator_exception const & ex) {
+//     formatter fmt = ios.get_formatter();
+//     options opts  = ios.get_options();
+//     auto j = ex.get_justification();
+//     j = remove_detail(j);
+//     regular(ios) << mk_pair(j.pp(fmt, opts, p, true), opts) << endl;
+// }
+
+// struct delta_pos_info_provider : public pos_info_provider {
+//     unsigned m_delta;
+//     std::string m_file_name;
+//     pos_info_provider const & m_provider;
+//     delta_pos_info_provider(unsigned d, char const * fname, pos_info_provider const & p):m_delta(d), m_file_name(fname), m_provider(p) {}
+//     virtual std::pair<unsigned, unsigned> get_pos_info(expr const & e) const {
+//         auto r = m_provider.get_pos_info(e);
+//         return mk_pair(r.first + m_delta, r.second);
+//     }
+//     virtual char const * get_file_name() const { return m_file_name.c_str(); }
+//     virtual std::pair<unsigned, unsigned> get_some_pos() const {
+//         auto r = m_provider.get_some_pos();
+//         return mk_pair(r.first + m_delta, r.second);
+//     }
+// };
 
-struct delta_pos_info_provider : public pos_info_provider {
-    unsigned m_delta;
-    std::string m_file_name;
-    pos_info_provider const & m_provider;
-    delta_pos_info_provider(unsigned d, char const * fname, pos_info_provider const & p):m_delta(d), m_file_name(fname), m_provider(p) {}
-    virtual std::pair<unsigned, unsigned> get_pos_info(expr const & e) const {
-        auto r = m_provider.get_pos_info(e);
-        return mk_pair(r.first + m_delta, r.second);
-    }
-    virtual char const * get_file_name() const { return m_file_name.c_str(); }
-    virtual std::pair<unsigned, unsigned> get_some_pos() const {
-        auto r = m_provider.get_some_pos();
-        return mk_pair(r.first + m_delta, r.second);
-    }
-};
 
 static void display_error(io_state const & ios, pos_info_provider const * p, script_exception const & ex) {
     if (p) {
@@ -98,8 +99,6 @@ static void display_error(io_state const & ios, pos_info_provider const * p, scr
     }
 }
 
-
-
 static void display_error(io_state const & ios, pos_info_provider const * p, script_nested_exception const & ex) {
     switch (ex.get_source()) {
     case script_exception::source::String:
@@ -125,53 +124,53 @@ static void display_error(io_state const & ios, pos_info_provider const * p, scr
     }
 }
 
-static void display_error(io_state const & ios, pos_info_provider const *, parser_nested_exception const & ex) {
-    display_error(ios, &(ex.get_provider()), ex.get_exception());
-}
+// static void display_error(io_state const & ios, pos_info_provider const *, parser_nested_exception const & ex) {
+//     display_error(ios, &(ex.get_provider()), ex.get_exception());
+// }
 
-static void display_error(io_state const & ios, pos_info_provider const *, parser_exception const & ex) {
-    regular(ios) << ex.what() << endl;
-}
+// static void display_error(io_state const & ios, pos_info_provider const *, parser_exception const & ex) {
+//     regular(ios) << ex.what() << endl;
+// }
 
-static void display_error(io_state const & ios, pos_info_provider const * p, unsolved_metavar_exception const & ex) {
-    display_error_pos(ios, p, ex.get_expr());
-    formatter fmt = ios.get_formatter();
-    options opts  = ios.get_options();
-    unsigned indent = get_pp_indent(opts);
-    format r = nest(indent, compose(line(), fmt(ex.get_expr(), opts)));
-    regular(ios) << " " << ex.what() << mk_pair(r, opts) << endl;
-    if (p) {
-        name_set already_displayed;
-        for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool {
-                if (is_metavar(e)) {
-                    name const & m = metavar_name(e);
-                    if (already_displayed.find(m) == already_displayed.end()) {
-                        already_displayed.insert(m);
-                        for (unsigned i = 0; i < indent; i++) regular(ios) << " ";
-                        display_error_pos(ios, p, e);
-                        regular(ios) << " unsolved metavar " << m << endl;
-                    }
-                }
-                return true;
-            });
-    }
-}
+// static void display_error(io_state const & ios, pos_info_provider const * p, unsolved_metavar_exception const & ex) {
+//     display_error_pos(ios, p, ex.get_expr());
+//     formatter fmt = ios.get_formatter();
+//     options opts  = ios.get_options();
+//     unsigned indent = get_pp_indent(opts);
+//     format r = nest(indent, compose(line(), fmt(ex.get_expr(), opts)));
+//     regular(ios) << " " << ex.what() << mk_pair(r, opts) << endl;
+//     if (p) {
+//         name_set already_displayed;
+//         for_each(ex.get_expr(), [&](expr const & e, unsigned) -> bool {
+//                 if (is_metavar(e)) {
+//                     name const & m = metavar_name(e);
+//                     if (already_displayed.find(m) == already_displayed.end()) {
+//                         already_displayed.insert(m);
+//                         for (unsigned i = 0; i < indent; i++) regular(ios) << " ";
+//                         display_error_pos(ios, p, e);
+//                         regular(ios) << " unsolved metavar " << m << endl;
+//                     }
+//                 }
+//                 return true;
+//             });
+//     }
+// }
 
 void display_error(io_state const & ios, pos_info_provider const * p, exception const & ex) {
     if (auto k_ex = dynamic_cast<kernel_exception const *>(&ex)) {
         display_error(ios, p, *k_ex);
-    } else if (auto e_ex = dynamic_cast<elaborator_exception const *>(&ex)) {
-        display_error(ios, p, *e_ex);
-    } else if (auto m_ex = dynamic_cast<unsolved_metavar_exception const *>(&ex)) {
-        display_error(ios, p, *m_ex);
+    // } else if (auto e_ex = dynamic_cast<elaborator_exception const *>(&ex)) {
+    //     display_error(ios, p, *e_ex);
+    // } else if (auto m_ex = dynamic_cast<unsolved_metavar_exception const *>(&ex)) {
+    //     display_error(ios, p, *m_ex);
     } else if (auto ls_ex = dynamic_cast<script_nested_exception const *>(&ex)) {
         display_error(ios, p, *ls_ex);
     } else if (auto s_ex = dynamic_cast<script_exception const *>(&ex)) {
         display_error(ios, p, *s_ex);
-    } else if (auto n_ex = dynamic_cast<parser_nested_exception const *>(&ex)) {
-        display_error(ios, p, *n_ex);
-    } else if (auto n_ex = dynamic_cast<parser_exception const *>(&ex)) {
-        display_error(ios, p, *n_ex);
+    // } else if (auto n_ex = dynamic_cast<parser_nested_exception const *>(&ex)) {
+    //     display_error(ios, p, *n_ex);
+    // } else if (auto n_ex = dynamic_cast<parser_exception const *>(&ex)) {
+    //     display_error(ios, p, *n_ex);
     } else if (p) {
         display_error_pos(ios, p->get_file_name(), p->get_some_pos().first, p->get_some_pos().second);
         regular(ios) << " " << ex.what() << endl;
diff --git a/src/library/error_handling/error_handling.h b/src/library/error_handling/error_handling.h
index 5e94427a3..feaebacca 100644
--- a/src/library/error_handling/error_handling.h
+++ b/src/library/error_handling/error_handling.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/exception.h"
 #include "kernel/pos_info_provider.h"
-#include "kernel/io_state.h"
+#include "library/io_state.h"
 
 namespace lean {
 /**
diff --git a/src/library/io_state_stream.cpp b/src/library/io_state_stream.cpp
index a3b1527ab..cdabdc6d2 100644
--- a/src/library/io_state_stream.cpp
+++ b/src/library/io_state_stream.cpp
@@ -18,18 +18,6 @@ io_state_stream const & operator<<(io_state_stream const & out, expr const & e)
     return out;
 }
 
-io_state_stream const & operator<<(io_state_stream const & out, object const & obj) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(obj, opts), opts);
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, environment const & env) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(env, opts), opts);
-    return out;
-}
-
 io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) {
     options const & opts = out.get_options();
     out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts);
diff --git a/src/library/io_state_stream.h b/src/library/io_state_stream.h
index 9002b345b..f75fcf84a 100644
--- a/src/library/io_state_stream.h
+++ b/src/library/io_state_stream.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "kernel/io_state.h"
+#include "library/io_state.h"
 
 namespace lean {
 /**
@@ -50,8 +50,6 @@ class kernel_exception;
 
 io_state_stream const & operator<<(io_state_stream const & out, endl_class);
 io_state_stream const & operator<<(io_state_stream const & out, expr const & e);
-io_state_stream const & operator<<(io_state_stream const & out, object const & obj);
-io_state_stream const & operator<<(io_state_stream const & out, environment const & env);
 io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex);
 template<typename T> io_state_stream const & operator<<(io_state_stream const & out, T const & t) {
     out.get_stream() << t;
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 145f0eb96..1c06a59bf 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -1,5 +1,5 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
@@ -8,23 +8,9 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/sstream.h"
 #include "util/script_state.h"
-#include "kernel/expr.h"
-#include "kernel/context.h"
-#include "kernel/formatter.h"
-#include "kernel/environment.h"
-#include "kernel/metavar.h"
-#include "kernel/abstract.h"
-#include "kernel/free_vars.h"
-#include "kernel/for_each_fn.h"
-#include "kernel/instantiate.h"
-#include "kernel/occurs.h"
-#include "kernel/kernel.h"
-#include "kernel/io_state.h"
-#include "kernel/type_checker.h"
 #include "library/io_state_stream.h"
 #include "library/expr_lt.h"
 #include "library/kernel_bindings.h"
-#include "library/printer.h"
 
 // Lua Bindings for the Kernel classes. We do not include the Lua
 // bindings in the kernel because we do not want to inflate the Kernel.
@@ -46,30 +32,17 @@ static int level_eq(lua_State * L) {
 }
 
 static int level_lt(lua_State * L) {
-    lua_pushboolean(L, to_level(L, 1) < to_level(L, 2));
+    lua_pushboolean(L, is_lt(to_level(L, 1), to_level(L, 2)));
     return 1;
 }
 
-static int mk_level(lua_State * L) {
-    int nargs = lua_gettop(L);
-    if (nargs == 0) {
-        // bottom
-        return push_level(L, level());
-    } else if (nargs == 1) {
-        // uvar
-        return push_level(L, level(to_name_ext(L, 1)));
-    } else if (nargs == 2 && lua_isnumber(L, 2)) {
-        // lift
-        return push_level(L, to_level(L, 1) + luaL_checkinteger(L, 2));
-    } else {
-        // max
-        level r = to_level(L, 1);
-        for (int i = 2; i <= nargs; i++) {
-            r = max(r, to_level(L, i));
-        }
-        return push_level(L, r);
-    }
-}
+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))); }
+static int mk_level_max(lua_State * L)  { return push_level(L, mk_max(to_level(L, 1), to_level(L, 2))); }
+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)    {      \
@@ -77,10 +50,69 @@ static int level_ ## P(lua_State * L)    {      \
     return 1;                                   \
 }
 
-LEVEL_PRED(is_bottom)
-LEVEL_PRED(is_uvar)
-LEVEL_PRED(is_lift)
+LEVEL_PRED(is_zero)
+LEVEL_PRED(is_param)
+LEVEL_PRED(is_meta)
+LEVEL_PRED(is_succ)
 LEVEL_PRED(is_max)
+LEVEL_PRED(is_imax)
+
+static int level_get_kind(lua_State * L) {
+    lua_pushinteger(L, static_cast<int>(kind(to_level(L, 1))));
+    return 1;
+}
+
+static const struct luaL_Reg level_m[] = {
+    {"__gc",            level_gc}, // never throws
+    {"__tostring",      safe_function<level_tostring>},
+    {"__eq",            safe_function<level_eq>},
+    {"__lt",            safe_function<level_lt>},
+    {"kind",            safe_function<level_get_kind>},
+    {"is_zero",         safe_function<level_is_zero>},
+    {"is_param",        safe_function<level_is_param>},
+    {"is_meta",         safe_function<level_is_meta>},
+    {"is_succ",         safe_function<level_is_succ>},
+    {"is_max",          safe_function<level_is_max>},
+    {"is_imax",         safe_function<level_is_imax>},
+    {"succ",            safe_function<mk_level_succ>},
+    {0, 0}
+};
+
+static void open_level(lua_State * L) {
+    luaL_newmetatable(L, level_mt);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, level_m, 0);
+
+    SET_GLOBAL_FUN(mk_level_zero,  "level");
+    SET_GLOBAL_FUN(mk_level_zero,  "mk_level_zero");
+    SET_GLOBAL_FUN(mk_level_one,   "mk_level_one");
+    SET_GLOBAL_FUN(mk_level_succ,  "mk_level_succ");
+    SET_GLOBAL_FUN(mk_level_max,   "mk_level_max");
+    SET_GLOBAL_FUN(mk_level_imax,  "mk_level_imax");
+    SET_GLOBAL_FUN(mk_param_univ,  "mk_param_univ");
+    SET_GLOBAL_FUN(mk_meta_univ,   "mk_meta_univ");
+
+    SET_GLOBAL_FUN(level_pred, "is_level");
+
+    lua_newtable(L);
+    SET_ENUM("Zero",      level_kind::Zero);
+    SET_ENUM("Succ",      level_kind::Succ);
+    SET_ENUM("Max",       level_kind::Max);
+    SET_ENUM("IMax",      level_kind::IMax);
+    SET_ENUM("Param",     level_kind::Param);
+    SET_ENUM("Meta",      level_kind::Meta);
+    lua_setglobal(L, "level_kind");
+}
+
+void open_kernel_module(lua_State * L) {
+    // TODO(Leo)
+    open_level(L);
+}
+}
+
+#if 0
+namespace lean {
 
 static int level_name(lua_State * L) {
     if (!is_uvar(to_level(L, 1)))
@@ -114,160 +146,6 @@ static int level_max_level(lua_State * L) {
     return push_level(L, max_level(to_level(L, 1), luaL_checkinteger(L, 2)));
 }
 
-static int level_get_kind(lua_State * L) {
-    lua_pushinteger(L, static_cast<int>(kind(to_level(L, 1))));
-    return 1;
-}
-
-static const struct luaL_Reg level_m[] = {
-    {"__gc",            level_gc}, // never throws
-    {"__tostring",      safe_function<level_tostring>},
-    {"__eq",            safe_function<level_eq>},
-    {"__lt",            safe_function<level_lt>},
-    {"kind",            safe_function<level_get_kind>},
-    {"is_bottom",       safe_function<level_is_bottom>},
-    {"is_lift",         safe_function<level_is_lift>},
-    {"is_max",          safe_function<level_is_max>},
-    {"is_uvar",         safe_function<level_is_uvar>},
-    {"uvar_name",       safe_function<level_name>},
-    {"lift_of",         safe_function<level_lift_of>},
-    {"lift_offset",     safe_function<level_lift_offset>},
-    {"max_size",        safe_function<level_max_size>},
-    {"max_level",       safe_function<level_max_level>},
-    {0, 0}
-};
-
-static void open_level(lua_State * L) {
-    luaL_newmetatable(L, level_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, level_m, 0);
-
-    SET_GLOBAL_FUN(mk_level,   "level");
-    SET_GLOBAL_FUN(level_pred, "is_level");
-
-    lua_newtable(L);
-    SET_ENUM("UVar",      level_kind::UVar);
-    SET_ENUM("Lift",      level_kind::Lift);
-    SET_ENUM("Max",       level_kind::Max);
-    lua_setglobal(L, "level_kind");
-}
-
-DECL_UDATA(local_entry)
-
-static int local_entry_eq(lua_State * L) {
-    lua_pushboolean(L, to_local_entry(L, 1) == to_local_entry(L, 2));
-    return 1;
-}
-
-static int local_entry_mk_lift(lua_State * L) {
-    return push_local_entry(L, mk_lift(luaL_checkinteger(L, 1), luaL_checkinteger(L, 2)));
-}
-
-static int local_entry_mk_inst(lua_State * L) {
-    return push_local_entry(L, mk_inst(luaL_checkinteger(L, 1), to_expr(L, 2)));
-}
-
-static int local_entry_is_lift(lua_State * L) {
-    lua_pushboolean(L, is_local_entry(L, 1) && to_local_entry(L, 1).is_lift());
-    return 1;
-}
-
-static int local_entry_is_inst(lua_State * L) {
-    lua_pushboolean(L, is_local_entry(L, 1) && to_local_entry(L, 1).is_inst());
-    return 1;
-}
-
-static int local_entry_s(lua_State * L) {
-    lua_pushinteger(L, to_local_entry(L, 1).s());
-    return 1;
-}
-
-static int local_entry_n(lua_State * L) {
-    local_entry & e = to_local_entry(L, 1);
-    if (!e.is_lift())
-        throw exception("Lean lift local entry expected");
-    lua_pushinteger(L, to_local_entry(L, 1).n());
-    return 1;
-}
-
-static int local_entry_v(lua_State * L) {
-    local_entry & e = to_local_entry(L, 1);
-    if (!e.is_inst())
-        throw exception("Lean inst local entry expected");
-    return push_expr(L, to_local_entry(L, 1).v());
-    return 1;
-}
-
-static const struct luaL_Reg local_entry_m[] = {
-    {"__gc",      local_entry_gc}, // never throws
-    {"__eq",      safe_function<local_entry_eq>},
-    {"is_lift",   safe_function<local_entry_is_lift>},
-    {"is_inst",   safe_function<local_entry_is_inst>},
-    {"s",         safe_function<local_entry_s>},
-    {"n",         safe_function<local_entry_n>},
-    {"v",         safe_function<local_entry_v>},
-    {0, 0}
-};
-
-DECL_UDATA(local_context)
-
-static int mk_local_context(lua_State * L) {
-    int nargs = lua_gettop(L);
-    if (nargs == 0) {
-        return push_local_context(L, local_context());
-    } else {
-        return push_local_context(L, local_context(to_local_entry(L, 1), to_local_context(L, 2)));
-    }
-}
-
-static int local_context_head(lua_State * L) {
-    return push_local_entry(L, head(to_local_context(L, 1)));
-}
-
-static int local_context_tail(lua_State * L) {
-    return push_local_context(L, tail(to_local_context(L, 1)));
-}
-
-static int local_context_is_nil(lua_State * L) {
-    lua_pushboolean(L, !to_local_context(L, 1));
-    return 1;
-}
-
-static const struct luaL_Reg local_context_m[] = {
-    {"__gc",      local_context_gc},
-    {"head",      local_context_head},
-    {"tail",      local_context_tail},
-    {"is_nil",    local_context_is_nil},
-    {0, 0}
-};
-
-static void local_entry_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_local_entry(tgt, to_local_entry(src, i));
-}
-
-static void local_context_migrate(lua_State * src, int i, lua_State * tgt) {
-    push_local_context(tgt, to_local_context(src, i));
-}
-
-static void open_local_context(lua_State * L) {
-    luaL_newmetatable(L, local_entry_mt);
-    set_migrate_fn_field(L, -1, local_entry_migrate);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, local_entry_m, 0);
-    SET_GLOBAL_FUN(local_entry_mk_lift, "mk_lift");
-    SET_GLOBAL_FUN(local_entry_mk_inst, "mk_inst");
-    SET_GLOBAL_FUN(local_entry_pred,    "is_local_entry");
-
-    luaL_newmetatable(L, local_context_mt);
-    set_migrate_fn_field(L, -1, local_context_migrate);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, local_context_m, 0);
-    SET_GLOBAL_FUN(mk_local_context,   "local_context");
-    SET_GLOBAL_FUN(local_context_pred, "is_local_context");
-}
 
 DECL_UDATA(expr)
 
@@ -1963,3 +1841,4 @@ void open_kernel_module(lua_State * L) {
     open_io_state(L);
 }
 }
+#endif
diff --git a/src/library/kernel_bindings.h b/src/library/kernel_bindings.h
index 3b25521c3..a35adae65 100644
--- a/src/library/kernel_bindings.h
+++ b/src/library/kernel_bindings.h
@@ -1,31 +1,27 @@
 /*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
 #pragma once
 #include "util/lua.h"
-#include "kernel/threadsafe_environment.h"
+#include "kernel/environment.h"
 
 namespace lean {
 void open_kernel_module(lua_State * L);
 UDATA_DEFS(level)
-UDATA_DEFS(local_entry)
-UDATA_DEFS_CORE(local_context)
 UDATA_DEFS(expr);
-UDATA_DEFS(context_entry)
-UDATA_DEFS(context)
 UDATA_DEFS(formatter)
-UDATA_DEFS(object)
+UDATA_DEFS(definition)
 UDATA_DEFS(environment)
 UDATA_DEFS(justification)
-UDATA_DEFS(metavar_env)
+UDATA_DEFS(constraint)
+UDATA_DEFS(substitution)
 UDATA_DEFS(io_state)
-int push_environment(lua_State * L, ro_environment const & env);
 int push_optional_expr(lua_State * L, optional<expr> const & e);
 int push_optional_justification(lua_State * L, optional<justification> const & j);
-int push_optional_object(lua_State * L, optional<object> const & o);
+int push_optional_definition(lua_State * L, optional<definition> const & o);
 /**
    \brief Return the formatter object associated with the given Lua State.
    This procedure checks for options at:
@@ -58,26 +54,6 @@ public:
     ~set_environment();
 };
 
-/**
-   \brief Helper class for getting a read-only reference
-   for an environment object on the Lua stack.
-*/
-class ro_shared_environment : public read_only_shared_environment {
-public:
-    ro_shared_environment(lua_State * L, int idx);
-    ro_shared_environment(lua_State * L);
-};
-
-/**
-   \brief Helper class for getting a read-write reference
-   for an environment object on the Lua stack.
-*/
-class rw_shared_environment : public read_write_shared_environment {
-public:
-    rw_shared_environment(lua_State * L, int idx);
-    rw_shared_environment(lua_State * L);
-};
-
 /** \brief Set the Lua registry of a Lua state with an io_state object. */
 void set_global_io_state(lua_State * L, io_state & ios);
 /**
diff --git a/src/library/register_module.h b/src/library/register_module.h
index 65a7cf425..4a40364c3 100644
--- a/src/library/register_module.h
+++ b/src/library/register_module.h
@@ -7,18 +7,18 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/script_state.h"
 #include "library/kernel_bindings.h"
-#include "library/substitution.h"
-#include "library/fo_unify.h"
-#include "library/hop_match.h"
-#include "library/placeholder.h"
+// #include "library/substitution.h"
+// #include "library/fo_unify.h"
+// #include "library/hop_match.h"
+// #include "library/placeholder.h"
 
 namespace lean {
 inline void open_core_module(lua_State * L) {
     open_kernel_module(L);
-    open_substitution(L);
-    open_fo_unify(L);
-    open_placeholder(L);
-    open_hop_match(L);
+    // open_substitution(L);
+    // open_fo_unify(L);
+    // open_placeholder(L);
+    // open_hop_match(L);
 }
 inline void register_core_module() {
     script_state::register_module(open_core_module);
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 371db206d..2eb95dbb5 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -19,12 +19,12 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/formatter.h"
+#include "library/error_handling/error_handling.h"
 #if 0
 #include "kernel/io_state.h"
 #include "library/printer.h"
 #include "library/kernel_bindings.h"
 #include "library/io_state_stream.h"
-#include "library/error_handling/error_handling.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/shell.h"
 #include "frontends/lean/frontend.h"
@@ -36,6 +36,7 @@ Author: Leonardo de Moura
 
 using lean::script_state;
 using lean::unreachable_reached;
+using lean::io_state;
 
 #if 0
 using lean::shell;
@@ -43,7 +44,6 @@ using lean::parser;
 using lean::invoke_debugger;
 using lean::notify_assertion_violation;
 using lean::environment;
-using lean::io_state;
 #endif
 
 enum class input_kind { Unspecified, Lean, OLean, Lua };
@@ -175,6 +175,7 @@ int main(int argc, char ** argv) {
         }
     }
 
+    io_state ios(lean::mk_simple_formatter());
     // environment env;
     // env->set_trusted_imported(trust_imported);
     // io_state ios = init_frontend(env, no_kernel);
@@ -237,7 +238,7 @@ int main(int argc, char ** argv) {
                     try {
                         S.dofile(argv[i]);
                     } catch (lean::exception & ex) {
-                        // ::lean::display_error(ios, nullptr, ex);
+                        ::lean::display_error(ios, nullptr, ex);
                         ok = false;
                     }
                 } else {