diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp
index cbe365c6c..bf5a79bdf 100644
--- a/src/api/api_ast.cpp
+++ b/src/api/api_ast.cpp
@@ -33,6 +33,7 @@ Revision History:
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/rewriter/expr_safe_replace.h"
+#include "ast/rewriter/recfun_replace.h"
 #include "ast/pp.h"
 #include "util/scoped_ctrl_c.h"
 #include "util/cancel_eh.h"
@@ -156,7 +157,8 @@ extern "C" {
             SET_ERROR_CODE(Z3_INVALID_ARG, nullptr);            
             return;
         }
-        p.set_definition(pd, n, _vars.c_ptr(), abs_body);
+        recfun_replace replace(m);
+        p.set_definition(replace, pd, n, _vars.c_ptr(), abs_body);
         Z3_CATCH;
     }
 
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index 7fe7ae00b..1ac44067f 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -21,7 +21,6 @@ Revision History:
 #include <functional>
 #include <sstream>
 #include "ast/expr_functors.h"
-#include "ast/expr_substitution.h"
 #include "ast/recfun_decl_plugin.h"
 #include "ast/ast_pp.h"
 #include "util/scoped_ptr_vector.h"
@@ -162,7 +161,7 @@ namespace recfun {
     static void convert_path(ast_manager & m,
                       choice_lst const * choices,
                       expr_ref_vector & conditions /* out */,
-                      expr_substitution & subst /* out */)
+                      replace & subst /* out */)
     {
         for (; choices != nullptr; choices = choices->next) {
             app * ite = choices->ite;
@@ -177,15 +176,6 @@ namespace recfun {
         }
     }
 
-    // substitute `subst` in `e`
-    static expr_ref replace_subst(th_rewriter & th_rw, ast_manager & m,
-                                  expr_substitution & subst, expr * e) {
-        th_rw.reset();
-        th_rw.set_substitution(&subst);
-        expr_ref res(m);
-        th_rw(e, res);
-        return res;
-    }
 
     void def::add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr * rhs, bool is_imm) {
         case_def c(m, m_fid, this, name, case_index, get_domain(), conditions, rhs);
@@ -198,7 +188,8 @@ namespace recfun {
 
 
     // Compute a set of cases, given the RHS
-    void def::compute_cases(is_immediate_pred & is_i, th_rewriter & th_rw,
+    void def::compute_cases(replace& subst, 
+                            is_immediate_pred & is_i, 
                             unsigned n_vars, var *const * vars, expr* rhs)
     {
         VERIFY(m_cases.empty() && "cases cannot already be computed");
@@ -291,13 +282,13 @@ namespace recfun {
                 // leaf of the search tree
 
                 conditions.reset();
-                expr_substitution subst(m);
+                subst.reset();
                 convert_path(m, b.path, conditions, subst);
                 
                 // substitute, to get rid of `ite` terms
-                expr_ref case_rhs = replace_subst(th_rw, m, subst, rhs);
+                expr_ref case_rhs = subst(rhs);
                 for (unsigned i = 0; i < conditions.size(); ++i) {
-                    conditions[i] = replace_subst(th_rw, m, subst, conditions.get(i));
+                    conditions[i] = subst(conditions.get(i));
                 }
                 
                 // yield new case
@@ -314,7 +305,7 @@ namespace recfun {
      */
 
     util::util(ast_manager & m)
-        : m_manager(m), m_fid(m.get_family_id("recfun")), m_th_rw(m),
+        : m_manager(m), m_fid(m.get_family_id("recfun")),
           m_plugin(dynamic_cast<decl::plugin*>(m.get_plugin(m_fid))) {
     }
 
@@ -325,8 +316,8 @@ namespace recfun {
         return alloc(def, m(), m_fid, name, n, domain, range);
     }
 
-    void util::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
-        d.set_definition(n_vars, vars, rhs);
+    void util::set_definition(replace& subst, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
+        d.set_definition(subst, n_vars, vars, rhs);
     }
 
     app_ref util::mk_depth_limit_pred(unsigned d) {
@@ -361,11 +352,11 @@ namespace recfun {
     };
 
     // set definition 
-    void promise_def::set_definition(unsigned n_vars, var * const * vars, expr * rhs) {
+    void promise_def::set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs) {
         SASSERT(n_vars == d->get_arity());
                     
         is_imm_pred is_i(*u);
-        d->compute_cases(is_i, u->get_th_rewriter(), n_vars, vars, rhs);
+        d->compute_cases(r, is_i, n_vars, vars, rhs);
     }
 
     namespace decl {
@@ -398,8 +389,8 @@ namespace recfun {
             return promise_def(&u(), d);
         }
         
-        void plugin::set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
-            u().set_definition(d, n_vars, vars, rhs);
+        void plugin::set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs) {
+            u().set_definition(r, d, n_vars, vars, rhs);
             for (case_def & c : d.get_def()->get_cases()) {
                 m_case_defs.insert(c.get_decl(), &c);
             }
@@ -409,11 +400,12 @@ namespace recfun {
             return !m_case_defs.empty();            
         }
 
-        def* plugin::mk_def(symbol const& name, unsigned n, sort ** params, sort * range,
+        def* plugin::mk_def(replace& subst, 
+                            symbol const& name, unsigned n, sort ** params, sort * range,
                             unsigned n_vars, var ** vars, expr * rhs) {
             promise_def d = mk_def(name, n, params, range);
             SASSERT(! m_defs.contains(d.get_def()->get_decl()));
-            set_definition(d, n_vars, vars, rhs);
+            set_definition(subst, d, n_vars, vars, rhs);
             return d.get_def();
         }
 
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index 347689a37..0247335e8 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -20,7 +20,6 @@ Revision History:
 #pragma once
 
 #include "ast/ast.h"
-#include "ast/rewriter/th_rewriter.h"
 #include "util/obj_hashtable.h"
 
 namespace recfun {
@@ -46,6 +45,13 @@ namespace recfun {
 
     typedef var_ref_vector vars;
 
+    class replace {
+    public:
+        virtual void reset() = 0;
+        virtual void insert(expr* d, expr* r) = 0;
+        virtual expr_ref operator()(expr* e) = 0;
+    };
+
     class case_def {
         friend class def;
         func_decl_ref       m_pred; //<! predicate used for this case
@@ -105,7 +111,7 @@ namespace recfun {
         def(ast_manager &m, family_id fid, symbol const & s, unsigned arity, sort *const * domain, sort* range);
 
         // compute cases for a function, given its RHS (possibly containing `ite`).
-        void compute_cases(is_immediate_pred &, th_rewriter & th_rw,
+        void compute_cases(replace& subst, is_immediate_pred &, 
                            unsigned n_vars, var *const * vars, expr* rhs);
         void add_case(std::string & name, unsigned case_index, expr_ref_vector const& conditions, expr* rhs, bool is_imm = false);
         bool contains_ite(expr* e); // expression contains a test?
@@ -129,7 +135,7 @@ namespace recfun {
         friend class util;
         util * u;
         def * d;
-        void set_definition(unsigned n_vars, var * const * vars, expr * rhs); // call only once
+        void set_definition(replace& r, unsigned n_vars, var * const * vars, expr * rhs); // call only once
     public:
         promise_def(util * u, def * d) : u(u), d(d) {}
         promise_def(promise_def const & from) : u(from.u), d(from.d) {}
@@ -167,9 +173,9 @@ namespace recfun {
             
             promise_def mk_def(symbol const& name, unsigned n, sort *const * params, sort * range);
             
-            void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
+            void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
             
-            def* mk_def(symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
+            def* mk_def(replace& subst, symbol const& name, unsigned n, sort ** params, sort * range, unsigned n_vars, var ** vars, expr * rhs);
 
             bool has_def(func_decl* f) const { return m_defs.contains(f); }
             bool has_defs() const;
@@ -193,18 +199,16 @@ namespace recfun {
         
         ast_manager &           m_manager;
         family_id               m_fid;
-        th_rewriter             m_th_rw;
         decl::plugin *          m_plugin;
 
         bool compute_is_immediate(expr * rhs);
-        void set_definition(promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
+        void set_definition(replace& r, promise_def & d, unsigned n_vars, var * const * vars, expr * rhs);
 
     public:
         util(ast_manager &m);
         ~util();
 
         ast_manager & m() { return m_manager; }
-        th_rewriter & get_th_rewriter() { return m_th_rw; }
         decl::plugin& get_plugin() { return *m_plugin; }
 
         bool is_case_pred(expr * e) const { return is_app_of(e, m_fid, OP_FUN_CASE_PRED); }
diff --git a/src/ast/rewriter/expr_safe_replace.cpp b/src/ast/rewriter/expr_safe_replace.cpp
index 0ed0efc00..e99568961 100644
--- a/src/ast/rewriter/expr_safe_replace.cpp
+++ b/src/ast/rewriter/expr_safe_replace.cpp
@@ -19,7 +19,6 @@ Revision History:
 --*/
 
 #include "ast/rewriter/expr_safe_replace.h"
-#include "ast/rewriter/rewriter.h"
 #include "ast/ast_pp.h"
 
 
diff --git a/src/ast/rewriter/expr_safe_replace.h b/src/ast/rewriter/expr_safe_replace.h
index fb66661af..3c7be4742 100644
--- a/src/ast/rewriter/expr_safe_replace.h
+++ b/src/ast/rewriter/expr_safe_replace.h
@@ -23,6 +23,7 @@ Revision History:
 #define EXPR_SAFE_REPLACE_H_
 
 #include "ast/ast.h"
+#include "ast/rewriter/var_subst.h"
 
 class expr_safe_replace {
     ast_manager& m;
diff --git a/src/ast/rewriter/recfun_replace.h b/src/ast/rewriter/recfun_replace.h
new file mode 100644
index 000000000..78dd0ee56
--- /dev/null
+++ b/src/ast/rewriter/recfun_replace.h
@@ -0,0 +1,41 @@
+/*++
+Copyright (c) 2018 Microsoft Corporation
+
+Module Name:
+
+    recfun_replace.h
+
+Abstract:
+
+    replace function for recfun.
+    recfun_decl_plugin relies on being able to do expression replacement.
+    It uses expr_safe_replace from ast/rewriter, which depends on ast.
+    To break the dependency cycle we hoist the relevant functionality into 
+    an argument to functionality exposed by recfun::set_definition
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2018-11-01
+
+Revision History:
+
+
+--*/
+
+#ifndef RECFUN_REPLACE_H_
+#define RECFUN_REPLACE_H_
+
+#include "ast/recfun_decl_plugin.h"
+#include "ast/rewriter/expr_safe_replace.h"
+
+class recfun_replace : public recfun::replace {
+    ast_manager& m;
+    expr_safe_replace m_replace;
+public:
+    recfun_replace(ast_manager& m): m(m), m_replace(m) {}
+    void reset() override { m_replace.reset(); }
+    void insert(expr* s, expr* t) { m_replace.insert(s, t); }
+    expr_ref operator()(expr* e) { expr_ref r(m); m_replace(e, r); return r; }
+};
+
+#endif /* RECFUN_REPLACE_H_ */
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index db0164445..250dbea08 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -39,6 +39,7 @@ Notes:
 #include "ast/well_sorted.h"
 #include "ast/for_each_expr.h"
 #include "ast/rewriter/th_rewriter.h"
+#include "ast/rewriter/recfun_replace.h"
 #include "model/model_evaluator.h"
 #include "model/model_smt2_pp.h"
 #include "model/model_v2_pp.h"
@@ -953,7 +954,8 @@ void cmd_context::insert_rec_fun(func_decl* f, expr_ref_vector const& binding, s
     }
     
     recfun::promise_def d = p.get_promise_def(f);
-    p.set_definition(d, vars.size(), vars.c_ptr(), rhs);
+    recfun_replace replace(m());
+    p.set_definition(replace, d, vars.size(), vars.c_ptr(), rhs);
 }
 
 func_decl * cmd_context::find_func_decl(symbol const & s) const {