diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp
index 6a2d4068c7..d57825b07f 100644
--- a/src/library/blast/blast.cpp
+++ b/src/library/blast/blast.cpp
@@ -756,10 +756,11 @@ void scope_assignment::commit() {
 }
 
 struct scope_debug::imp {
-    scope_hash_consing m_scope1;
-    blastenv           m_benv;
-    scope_blastenv     m_scope2;
+    scoped_expr_caching m_scope1;
+    blastenv            m_benv;
+    scope_blastenv      m_scope2;
     imp(environment const & env, io_state const & ios):
+        m_scope1(true),
         m_benv(env, ios, list<name>(), list<name>()),
         m_scope2(m_benv) {
         expr aux_mvar = mk_metavar("dummy_mvar", mk_true());
@@ -847,7 +848,7 @@ expr internalize(expr const & e) {
 }
 optional<expr> blast_goal(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds,
                           goal const & g) {
-    blast::scope_hash_consing scope1;
+    scoped_expr_caching      scope1(true);
     blast::blastenv b(env, ios, ls, ds);
     blast::scope_blastenv    scope2(b);
     return b(g);
diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp
index ad39b5db0d..17660aa340 100644
--- a/src/library/blast/expr.cpp
+++ b/src/library/blast/expr.cpp
@@ -13,34 +13,11 @@ Author: Leonardo de Moura
 #include "kernel/instantiate_univ_cache.h"
 #include "library/blast/expr.h"
 
-#ifndef LEAN_BLAST_INST_UNIV_CACHE_SIZE
-#define LEAN_BLAST_INST_UNIV_CACHE_SIZE 1023
-#endif
-
 namespace lean {
 namespace blast {
 static name * g_prefix = nullptr;
 static expr * g_dummy_type = nullptr; // dummy type for href/mref
 
-typedef typename std::vector<expr> expr_array;
-LEAN_THREAD_PTR(expr_array,  g_mref_array);
-LEAN_THREAD_PTR(expr_array,  g_href_array);
-
-scope_hash_consing::scope_hash_consing():
-    scoped_expr_caching(true) {
-    lean_assert(g_mref_array  == nullptr);
-    lean_assert(g_href_array  == nullptr);
-    g_mref_array  = new expr_array();
-    g_href_array  = new expr_array();
-}
-
-scope_hash_consing::~scope_hash_consing() {
-    delete g_mref_array;
-    delete g_href_array;
-    g_mref_array  = nullptr;
-    g_href_array  = nullptr;
-}
-
 level mk_uref(unsigned idx) {
     return lean::mk_meta_univ(name(*g_prefix, idx));
 }
@@ -54,38 +31,16 @@ unsigned uref_index(level const & l) {
     return meta_id(l).get_numeral();
 }
 
-static expr mk_href_core(unsigned idx) {
-    return lean::mk_local(name(*g_prefix, idx), *g_dummy_type);
-}
-
 expr mk_href(unsigned idx) {
-    lean_assert(g_href_array);
-    while (g_href_array->size() <= idx) {
-        unsigned j   = g_href_array->size();
-        expr new_ref = mk_href_core(j);
-        g_href_array->push_back(new_ref);
-    }
-    lean_assert(idx < g_href_array->size());
-    return (*g_href_array)[idx];
+    return lean::mk_local(name(*g_prefix, idx), *g_dummy_type);
 }
 
 bool is_href(expr const & e) {
     return lean::is_local(e) && mlocal_type(e) == *g_dummy_type;
 }
 
-static expr mk_mref_core(unsigned idx) {
-    return mk_metavar(name(*g_prefix, idx), *g_dummy_type);
-}
-
 expr mk_mref(unsigned idx) {
-    lean_assert(g_mref_array);
-    while (g_mref_array->size() <= idx) {
-        unsigned j   = g_mref_array->size();
-        expr new_ref = mk_mref_core(j);
-        g_mref_array->push_back(new_ref);
-    }
-    lean_assert(idx < g_mref_array->size());
-    return (*g_mref_array)[idx];
+    return mk_metavar(name(*g_prefix, idx), *g_dummy_type);
 }
 
 bool is_mref(expr const & e) {
diff --git a/src/library/blast/expr.h b/src/library/blast/expr.h
index 98c35f4806..0fb60541db 100644
--- a/src/library/blast/expr.h
+++ b/src/library/blast/expr.h
@@ -10,22 +10,6 @@ Author: Leonardo de Moura
 
 namespace lean {
 namespace blast {
-// API for creating maximally shared terms used by the blast tactic.
-// The API assumes there is a single blast tactic using theses terms.
-// The expression hash-consing tables are thread local and implemented
-// in the kernel
-
-// Remark: All procedures assume the children levels and expressions are maximally shared.
-// That is, it assumes they have been created using the APIs provided by this module.
-
-// Auxiliary object for resetting the the thread local hash-consing tables.
-// It also uses an assertion to make sure it is not being used in a recursion.
-class scope_hash_consing : public scoped_expr_caching {
-public:
-    scope_hash_consing();
-    ~scope_hash_consing();
-};
-
 level mk_uref(unsigned idx);
 
 bool is_uref(level const & l);
@@ -45,9 +29,7 @@ bool has_href(expr const & e);
 /** \brief Return true iff \c e contain mref's */
 bool has_mref(expr const & e);
 
-inline bool is_local_non_href(expr const & e) {
-    return is_local(e) && !is_href(e);
-}
+inline bool is_local_non_href(expr const & e) { return is_local(e) && !is_href(e); }
 
 void initialize_expr();
 void finalize_expr();