diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt
index f2882f7fc..766c3f9be 100644
--- a/src/kernel/CMakeLists.txt
+++ b/src/kernel/CMakeLists.txt
@@ -3,6 +3,6 @@ replace_fn.cpp free_vars.cpp abstract.cpp instantiate.cpp
 formatter.cpp declaration.cpp environment.cpp
 justification.cpp pos_info_provider.cpp metavar.cpp converter.cpp
 constraint.cpp type_checker.cpp error_msgs.cpp kernel_exception.cpp
-normalizer_extension.cpp init_module.cpp extension_context.cpp)
+normalizer_extension.cpp init_module.cpp extension_context.cpp expr_cache.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})
diff --git a/src/kernel/expr_cache.cpp b/src/kernel/expr_cache.cpp
new file mode 100644
index 000000000..5b8dfd33c
--- /dev/null
+++ b/src/kernel/expr_cache.cpp
@@ -0,0 +1,33 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/expr_cache.h"
+
+namespace lean {
+expr * expr_cache::find(expr const & e) {
+    unsigned i = e.hash() % m_capacity;
+    if (m_cache[i].m_expr && is_bi_equal(*m_cache[i].m_expr, e))
+        return &m_cache[i].m_result;
+    else
+        return nullptr;
+}
+
+void expr_cache::insert(expr const & e, expr const & v) {
+    unsigned i = e.hash() % m_capacity;
+    if (!m_cache[i].m_expr)
+        m_used.push_back(i);
+    m_cache[i].m_expr   = e;
+    m_cache[i].m_result = v;
+}
+
+void expr_cache::clear() {
+    for (unsigned i : m_used) {
+        m_cache[i].m_expr   = none_expr();
+        m_cache[i].m_result = expr();
+    }
+    m_used.clear();
+}
+}
diff --git a/src/kernel/expr_cache.h b/src/kernel/expr_cache.h
new file mode 100644
index 000000000..e42aa18f7
--- /dev/null
+++ b/src/kernel/expr_cache.h
@@ -0,0 +1,31 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include <vector>
+#include "kernel/expr.h"
+
+namespace lean {
+/** \brief Cache for storing mappings from expressions to expressions.
+
+    \warning The insert(k, v) method overwrites andy entry (k1, v1) when
+    hash(k) == hash(k1)
+*/
+class expr_cache {
+    struct entry {
+        optional<expr> m_expr;
+        expr           m_result;
+    };
+    unsigned              m_capacity;
+    std::vector<entry>    m_cache;
+    std::vector<unsigned> m_used;
+public:
+    expr_cache(unsigned c):m_capacity(c), m_cache(c) {}
+    void insert(expr const & e, expr const & v);
+    expr * find(expr const & e);
+    void clear();
+};
+}
diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp
index c13fe249b..358b306cf 100644
--- a/src/kernel/metavar.cpp
+++ b/src/kernel/metavar.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "kernel/expr_maps.h"
 #include "kernel/level.h"
 #include "kernel/cache_stack.h"
+#include "kernel/expr_cache.h"
 
 #ifndef LEAN_INSTANTIATE_METAVARS_CACHE_CAPACITY
 #define LEAN_INSTANTIATE_METAVARS_CACHE_CAPACITY 1024*8
@@ -98,41 +99,7 @@ pair<level, justification> substitution::instantiate_metavars(level const & l, b
     return mk_pair(r, j);
 }
 
-struct instantiate_metavars_cache {
-    struct entry {
-        optional<expr> m_expr;
-        expr           m_result;
-    };
-    unsigned              m_capacity;
-    std::vector<entry>    m_cache;
-    std::vector<unsigned> m_used;
-    instantiate_metavars_cache(unsigned c):m_capacity(c), m_cache(c) {}
-
-    expr * find(expr const & e) {
-        unsigned i = e.hash() % m_capacity;
-        if (m_cache[i].m_expr && is_bi_equal(*m_cache[i].m_expr, e))
-            return &m_cache[i].m_result;
-        else
-            return nullptr;
-    }
-
-    void insert(expr const & e, expr const & v) {
-        unsigned i = e.hash() % m_capacity;
-        if (!m_cache[i].m_expr)
-            m_used.push_back(i);
-        m_cache[i].m_expr   = e;
-        m_cache[i].m_result = v;
-    }
-
-    void clear() {
-        for (unsigned i : m_used) {
-            m_cache[i].m_expr   = none_expr();
-            m_cache[i].m_result = expr();
-        }
-        m_used.clear();
-    }
-};
-
+typedef expr_cache instantiate_metavars_cache;
 MK_CACHE_STACK(instantiate_metavars_cache, LEAN_INSTANTIATE_METAVARS_CACHE_CAPACITY)
 
 class instantiate_metavars_fn {