diff --git a/src/library/type_context.h b/src/library/type_context.h
index cd02480098..c293276e45 100644
--- a/src/library/type_context.h
+++ b/src/library/type_context.h
@@ -376,6 +376,8 @@ public:
     bool is_prop(expr const & e);
     bool is_proof(expr const & e);
 
+    optional<expr> expand_macro(expr const & e);
+
     optional<name> is_class(expr const & type);
     optional<expr> mk_class_instance(expr const & type);
     optional<expr> mk_subsingleton_instance(expr const & type);
@@ -471,7 +473,6 @@ private:
     optional<expr> unfold_definition(expr const & e);
     optional<expr> try_unfold_definition(expr const & e);
     bool should_unfold_macro(expr const & e);
-    optional<expr> expand_macro(expr const & e);
     expr whnf_core(expr const & e);
     optional<declaration> is_transparent(transparency_mode m, name const & n);
     optional<declaration> is_transparent(name const & n);
diff --git a/src/library/unfold_macros.cpp b/src/library/unfold_macros.cpp
index 962ffae858..24651261bf 100644
--- a/src/library/unfold_macros.cpp
+++ b/src/library/unfold_macros.cpp
@@ -5,14 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/interrupt.h"
-#include "util/fresh_name.h"
-#include "kernel/type_checker.h"
 #include "kernel/find_fn.h"
 #include "kernel/expr_maps.h"
-#include "kernel/instantiate.h"
-#include "kernel/abstract.h"
+#include "library/type_context.h"
 #include "library/unfold_macros.h"
-#include "library/replace_visitor.h"
+#include "library/replace_visitor_with_tc.h"
 #include "library/exception.h"
 
 /* If the trust level of all macros is < LEAN_BELIEVER_TRUST_LEVEL,
@@ -21,26 +18,17 @@ Author: Leonardo de Moura
 // #define LEAN_ALL_MACROS_HAVE_SMALL_TRUST_LVL
 
 namespace lean {
-class unfold_untrusted_macros_fn {
-    typedef expr_bi_struct_map<expr> cache;
-
-    type_checker m_tc;
+class unfold_untrusted_macros_fn : public replace_visitor_with_tc {
     unsigned     m_trust_lvl;
-    cache        m_cache;
 
-    expr save_result(expr const & e, expr && r) {
-        m_cache.insert(std::make_pair(e, r));
-        return r;
-    }
-
-    expr visit_macro(expr const & e) {
+    virtual expr visit_macro(expr const & e) override {
         buffer<expr> new_args;
         for (unsigned i = 0; i < macro_num_args(e); i++)
             new_args.push_back(visit(macro_arg(e, i)));
         auto def = macro_def(e);
         expr r = update_macro(e, new_args.size(), new_args.data());
         if (def.trust_level() >= m_trust_lvl) {
-            if (optional<expr> new_r = m_tc.expand_macro(r)) {
+            if (optional<expr> new_r = m_ctx.expand_macro(r)) {
                 return *new_r;
             } else {
                 throw generic_exception(e, "failed to expand macro");
@@ -50,77 +38,9 @@ class unfold_untrusted_macros_fn {
         }
     }
 
-    expr visit_app(expr const & e) {
-        expr new_f = visit(app_fn(e));
-        expr new_v = visit(app_arg(e));
-        return update_app(e, new_f, new_v);
-    }
-
-    expr visit_binding(expr e) {
-        expr_kind k = e.kind();
-        buffer<expr>  es;
-        buffer<expr>  ls;
-        while (e.kind() == k) {
-            expr d = visit(instantiate_rev(binding_domain(e), ls.size(), ls.data()));
-            expr l = mk_local(mk_fresh_name(), binding_name(e), d, binding_info(e));
-            ls.push_back(l);
-            es.push_back(e);
-            e = binding_body(e);
-        }
-        e = visit(instantiate_rev(e, ls.size(), ls.data()));
-        expr r = abstract_locals(e, ls.size(), ls.data());
-        while (!ls.empty()) {
-            expr d = mlocal_type(ls.back());
-            ls.pop_back();
-            d = abstract_locals(d, ls.size(), ls.data());
-            r = update_binding(es.back(), d, r);
-            es.pop_back();
-        }
-        return r;
-    }
-
-    expr visit_let(expr const & e) {
-        // TODO(Leo): improve
-        return visit(instantiate(let_body(e), let_value(e)));
-    }
-
-    expr visit(expr const & e) {
-        switch (e.kind()) {
-        case expr_kind::Sort:  case expr_kind::Constant:
-        case expr_kind::Var:   case expr_kind::Meta:
-        case expr_kind::Local:
-            return e;
-        default:
-            break;
-        }
-
-        check_system("unfold macros");
-        auto it = m_cache.find(e);
-        if (it != m_cache.end())
-            return it->second;
-
-        switch (e.kind()) {
-        case expr_kind::Sort:  case expr_kind::Constant:
-        case expr_kind::Var:   case expr_kind::Meta:
-        case expr_kind::Local:
-            lean_unreachable();
-        case expr_kind::Macro:
-            return save_result(e, visit_macro(e));
-        case expr_kind::App:
-            return save_result(e, visit_app(e));
-        case expr_kind::Lambda: case expr_kind::Pi:
-            return save_result(e, visit_binding(e));
-        case expr_kind::Let:
-            return save_result(e, visit_let(e));
-        }
-        lean_unreachable();
-    }
-
 public:
-    unfold_untrusted_macros_fn(environment const & env, unsigned lvl):
-        m_tc(env), m_trust_lvl(lvl) {}
-
-    expr operator()(expr const & e) { return visit(e); }
+    unfold_untrusted_macros_fn(type_context & ctx, unsigned lvl):
+        replace_visitor_with_tc(ctx), m_trust_lvl(lvl) {}
 };
 
 static bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
@@ -134,7 +54,8 @@ static bool contains_untrusted_macro(unsigned trust_lvl, expr const & e) {
 
 expr unfold_untrusted_macros(environment const & env, expr const & e, unsigned trust_lvl) {
     if (contains_untrusted_macro(trust_lvl, e)) {
-        return unfold_untrusted_macros_fn(env, trust_lvl)(e);
+        type_context ctx(env, transparency_mode::All);
+        return unfold_untrusted_macros_fn(ctx, trust_lvl)(e);
     } else {
         return e;
     }