diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index b9466e89e9..ca6d01e085 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -19,4 +19,4 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   tmp_type_context.cpp fun_info_manager.cpp congr_lemma_manager.cpp
   abstract_expr_manager.cpp light_lt_manager.cpp trace.cpp
   attribute_manager.cpp error_handling.cpp unification_hint.cpp defeq_simp_lemmas.cpp
-  defeq_simplifier.cpp)
+  defeq_simplifier.cpp local_context.cpp)
diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp
new file mode 100644
index 0000000000..b24a38e261
--- /dev/null
+++ b/src/library/local_context.cpp
@@ -0,0 +1,95 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/fresh_name.h"
+#include "library/local_context.h"
+
+namespace lean {
+static name *       g_local_prefix;
+static expr *       g_dummy_type;
+static local_decl * g_dummy_decl;
+
+DEF_THREAD_MEMORY_POOL(get_local_decl_allocator, sizeof(local_decl::cell));
+
+void local_decl::cell::dealloc() {
+    this->~cell();
+    get_local_decl_allocator().recycle(this);
+}
+local_decl::cell::cell(name const & n, name const & pp_n, expr const & t, optional<expr> const & v, binder_info const & bi):
+    m_name(n), m_pp_name(pp_n), m_type(t), m_value(v), m_bi(bi), m_rc(1) {}
+
+local_decl::local_decl():local_decl(*g_dummy_decl) {}
+local_decl::local_decl(name const & n, name const & pp_n, expr const & t, optional<expr> const & v, binder_info const & bi) {
+    m_ptr = new (get_local_decl_allocator().allocate()) cell(n, pp_n, t, v, bi);
+}
+
+name mk_local_decl_name() {
+    return mk_tagged_fresh_name(*g_local_prefix);
+}
+
+expr mk_local_ref(name const & n) {
+    return mk_local(n, *g_dummy_type);
+}
+
+bool is_local_decl_ref(expr const & e) {
+    return is_local(e) && mlocal_type(e) == *g_dummy_type;
+}
+
+expr local_context::mk_local_decl(name const & n, name const & ppn, expr const & type, optional<expr> const & value, binder_info const & bi) {
+    lean_assert(!m_local_decl_map.contains(n));
+    local_decl l(n, ppn, type, value, bi);
+    m_local_decls = cons(l, m_local_decls);
+    m_local_decl_map.insert(n, l);
+    return mk_local_ref(n);
+}
+
+expr local_context::mk_local_decl(expr const & type, binder_info const & bi) {
+    name n = mk_local_decl_name();
+    return mk_local_decl(n, n, type, none_expr(), bi);
+}
+
+expr local_context::mk_local_decl(expr const & type, expr const & value) {
+    name n = mk_local_decl_name();
+    return mk_local_decl(n, n, type, some_expr(value), binder_info());
+}
+
+expr local_context::mk_local_decl(name const & ppn, expr const & type, binder_info const & bi) {
+    return mk_local_decl(mk_local_decl_name(), ppn, type, none_expr(), bi);
+}
+
+expr local_context::mk_local_decl(name const & ppn, expr const & type, expr const & value) {
+    return mk_local_decl(mk_local_decl_name(), ppn, type, some_expr(value), binder_info());
+}
+
+optional<local_decl> local_context::get_local_decl(expr const & e) {
+    lean_assert(is_local_decl_ref(e));
+    if (auto r = m_local_decl_map.find(mlocal_name(e)))
+        return optional<local_decl>(*r);
+    else
+        return optional<local_decl>();
+}
+
+void local_context::for_each(std::function<void(local_decl const &)> const & fn) const {
+    m_local_decl_map.for_each([&](name const &, local_decl const & d) { fn(d); });
+}
+
+optional<local_decl> local_context::find_if(std::function<bool(local_decl const &)> const & pred) const { // NOLINT
+    return m_local_decl_map.find_if([&](name const &, local_decl const & d) { return pred(d); });
+}
+
+void initialize_local_context() {
+    g_local_prefix = new name(name::mk_internal_unique_name());
+    g_dummy_type   = new expr(mk_constant(name::mk_internal_unique_name()));
+    g_dummy_decl   = new local_decl(name("__local_decl_for_default_constructor"), name("__local_decl_for_default_constructor"),
+                                    *g_dummy_type, optional<expr>(), binder_info());
+}
+
+void finalize_local_context() {
+    delete g_local_prefix;
+    delete g_dummy_type;
+    delete g_dummy_decl;
+}
+}
diff --git a/src/library/local_context.h b/src/library/local_context.h
new file mode 100644
index 0000000000..9ca452867e
--- /dev/null
+++ b/src/library/local_context.h
@@ -0,0 +1,69 @@
+/*
+Copyright (c) 2016 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/name_map.h"
+#include "kernel/expr.h"
+
+namespace lean {
+class local_decl {
+public:
+    struct cell {
+        /*
+          <name> : <type> := <value>
+
+          m_pp_name is used for interacting with the user.
+          It may not be not unique.
+        */
+        name               m_name; /* this one is unique */
+        name               m_pp_name;
+        expr               m_type;
+        optional<expr>     m_value;
+        binder_info        m_bi;
+        MK_LEAN_RC(); // Declare m_rc counter
+        void dealloc();
+        cell(name const & n, name const & pp_n, expr const & t, optional<expr> const & v, binder_info const & bi);
+    };
+private:
+    cell * m_ptr;
+    friend class local_context;
+public:
+    local_decl();
+    local_decl(name const & n, name const & pp_n, expr const & t, optional<expr> const & v, binder_info const & bi);
+    local_decl(local_decl const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
+    local_decl(local_decl && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
+    ~local_decl() { if (m_ptr) m_ptr->dec_ref(); }
+    local_decl & operator=(local_decl const & s) { LEAN_COPY_REF(s); }
+    local_decl & operator=(local_decl && s) { LEAN_MOVE_REF(s); }
+
+    friend bool is_eqp(local_decl const & a, local_decl const & b) { return a.m_ptr == b.m_ptr; }
+
+    name const & get_name() const { return m_ptr->m_name; }
+    name const & get_pp_name() const { return m_ptr->m_pp_name; }
+    expr const & get_type() const { return m_ptr->m_type; }
+    optional<expr> const & get_value() const { return m_ptr->m_value; }
+    binder_info const & get_info() const { return m_ptr->m_bi; }
+};
+
+bool is_local_decl_ref(expr const & e);
+
+class local_context {
+    name_map<local_decl> m_local_decl_map;
+    list<local_decl>     m_local_decls;
+    expr mk_local_decl(name const & n, name const & ppn, expr const & type, optional<expr> const & value, binder_info const & bi);
+public:
+    expr mk_local_decl(expr const & type, binder_info const & bi = binder_info());
+    expr mk_local_decl(expr const & type, expr const & value);
+    expr mk_local_decl(name const & ppn, expr const & type, binder_info const & bi = binder_info());
+    expr mk_local_decl(name const & ppn, expr const & type, expr const & value);
+    optional<local_decl> get_local_decl(expr const & e);
+    void for_each(std::function<void(local_decl const &)> const & fn) const;
+    optional<local_decl> find_if(std::function<bool(local_decl const &)> const & pred) const; // NOLINT
+};
+
+void initialize_local_context();
+void finalize_local_context();
+}
diff --git a/src/util/rb_map.h b/src/util/rb_map.h
index be28b41ed9..126a9a5248 100644
--- a/src/util/rb_map.h
+++ b/src/util/rb_map.h
@@ -76,7 +76,10 @@ public:
     template<typename F>
     optional<T> find_if(F && f) const {
         auto f_prime = [&](entry const & e) { return f(e.first, e.second); };
-        return m_map.find_if(f_prime);
+        if (auto r = m_map.find_if(f_prime))
+            return optional<T>(r->second);
+        else
+            return optional<T>();
     }
 
     /** \brief (For debugging) Display the content of this splay map. */