diff --git a/src/kernel/replace_fn.cpp b/src/kernel/replace_fn.cpp
index 4f9fd265ee..3c29845e3a 100644
--- a/src/kernel/replace_fn.cpp
+++ b/src/kernel/replace_fn.cpp
@@ -58,151 +58,6 @@ struct replace_cache {
 
 MK_CACHE_STACK(replace_cache, LEAN_DEFAULT_REPLACE_CACHE_CAPACITY)
 
-/**
-   \brief Functional for applying <tt>F</tt> to the subexpressions of a given expression.
-
-   The signature of \c F is
-   expr const &, unsigned -> optional(expr)
-
-   F is invoked for each subexpression \c s of the input expression e.
-   In a call <tt>F(s, n)</tt>, n is the scope level, i.e., the number of
-   bindings operators that enclosing \c s. The replaces only visits children of \c e
-   if F return none_expr
-*/
-class replace_fn {
-    struct frame {
-        expr       m_expr;
-        unsigned   m_offset;
-        bool       m_shared;
-        unsigned   m_index;
-        frame(expr const & e, unsigned o, bool s):m_expr(e), m_offset(o), m_shared(s), m_index(0) {}
-    };
-    typedef buffer<frame>  frame_stack;
-    typedef buffer<expr>   result_stack;
-
-    std::function<optional<expr>(expr const &, unsigned)> m_f;
-    frame_stack                                           m_fs;
-    result_stack                                          m_rs;
-    replace_cache_ref                                     m_cache;
-    bool                                                  m_use_cache;
-
-    void save_result(expr const & e, expr const & r, unsigned offset, bool shared) {
-        if (shared)
-            m_cache->insert(e, offset, r);
-        m_rs.push_back(r);
-    }
-
-    /**
-       \brief Visit \c e at the given offset. Return true iff the result is on the
-       result stack \c m_rs. Return false iff a new frame was pushed on the stack \c m_fs.
-       The idea is that after the frame is processed, the result will be on the result stack.
-    */
-    bool visit(expr const & e, unsigned offset) {
-        bool shared = false;
-        if (m_use_cache && is_shared(e)) {
-            if (auto r = m_cache->find(e, offset)) {
-                m_rs.push_back(*r);
-                return true;
-            }
-            shared = true;
-        }
-
-        optional<expr> r = m_f(e, offset);
-        if (r) {
-            save_result(e, *r, offset, shared);
-            return true;
-        } else if (is_atomic(e)) {
-            save_result(e, e, offset, shared);
-            return true;
-        } else {
-            m_fs.emplace_back(e, offset, shared);
-            return false;
-        }
-    }
-
-    /**
-       \brief Return true iff <tt>f.m_index == idx</tt>.
-       When the result is true, <tt>f.m_index</tt> is incremented.
-    */
-    bool check_index(frame & f, unsigned idx) {
-        if (f.m_index == idx) {
-            f.m_index++;
-            return true;
-        } else {
-            return false;
-        }
-    }
-
-    expr const & rs(int i) {
-        lean_assert(i < 0);
-        return m_rs[m_rs.size() + i];
-    }
-
-    void pop_rs(unsigned num) {
-        m_rs.shrink(m_rs.size() - num);
-    }
-
-public:
-    template<typename F>
-    replace_fn(F const & f, bool use_cache):m_f(f), m_use_cache(use_cache) {}
-
-    expr operator()(expr const & e) {
-        expr r;
-        visit(e, 0);
-        while (!m_fs.empty()) {
-          begin_loop:
-            check_interrupted();
-            check_memory("replace");
-            frame & f = m_fs.back();
-            expr const & e   = f.m_expr;
-            unsigned offset  = f.m_offset;
-            switch (e.kind()) {
-            case expr_kind::Constant: case expr_kind::Sort:
-            case expr_kind::Var:
-                lean_unreachable(); // LCOV_EXCL_LINE
-            case expr_kind::Meta:     case expr_kind::Local:
-                if (check_index(f, 0) && !visit(mlocal_type(e), offset))
-                    goto begin_loop;
-                r = update_mlocal(e, rs(-1));
-                pop_rs(1);
-                break;
-            case expr_kind::App:
-                if (check_index(f, 0) && !visit(app_fn(e), offset))
-                    goto begin_loop;
-                if (check_index(f, 1) && !visit(app_arg(e), offset))
-                    goto begin_loop;
-                r = update_app(e, rs(-2), rs(-1));
-                pop_rs(2);
-                break;
-            case expr_kind::Pi: case expr_kind::Lambda:
-                if (check_index(f, 0) && !visit(binding_domain(e), offset))
-                    goto begin_loop;
-                if (check_index(f, 1) && !visit(binding_body(e), offset + 1))
-                    goto begin_loop;
-                r = update_binding(e, rs(-2), rs(-1));
-                pop_rs(2);
-                break;
-            case expr_kind::Macro:
-                while (f.m_index < macro_num_args(e)) {
-                    unsigned idx = f.m_index;
-                    f.m_index++;
-                    if (!visit(macro_arg(e, idx), offset))
-                        goto begin_loop;
-                }
-                r = update_macro(e, macro_num_args(e), &rs(-macro_num_args(e)));
-                pop_rs(macro_num_args(e));
-                break;
-            }
-            save_result(e, r, offset, f.m_shared);
-            m_fs.pop_back();
-        }
-        lean_assert(m_rs.size() == 1);
-        r = m_rs.back();
-        m_rs.pop_back();
-        return r;
-    }
-};
-
 class replace_rec_fn {
     replace_cache_ref                                     m_cache;
     std::function<optional<expr>(expr const &, unsigned)> m_f;
@@ -262,9 +117,6 @@ public:
 };
 
 expr replace(expr const & e, std::function<optional<expr>(expr const &, unsigned)> const & f, bool use_cache) {
-    if (get_weight(e) < LEAN_REPLACE_SMALL_TERM_THRESHOLD)
-        return replace_rec_fn(f, use_cache)(e);
-    else
-        return replace_fn(f, use_cache)(e);
+    return replace_rec_fn(f, use_cache)(e);
 }
 }