diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt
index a8f7303e7..f6afd539f 100644
--- a/src/smt/CMakeLists.txt
+++ b/src/smt/CMakeLists.txt
@@ -10,7 +10,6 @@ z3_add_component(smt
     expr_context_simplifier.cpp
     fingerprints.cpp
     mam.cpp
-    model_sweeper.cpp
     old_interval.cpp
     qi_queue.cpp
     seq_axioms.cpp
diff --git a/src/smt/theory_recfun.cpp b/src/smt/theory_recfun.cpp
index fa3331816..cfe4522de 100644
--- a/src/smt/theory_recfun.cpp
+++ b/src/smt/theory_recfun.cpp
@@ -22,7 +22,6 @@ Revision History:
 #include "ast/for_each_expr.h"
 #include "smt/theory_recfun.h"
 #include "smt/params/smt_params_helper.hpp"
-#include "smt/model_sweeper.h"
 
 
 #define TRACEFN(x) TRACE("recfun", tout << x << '\n';)
@@ -444,7 +443,6 @@ namespace smt {
     final_check_status theory_recfun::final_check_eh() {
         TRACEFN("final\n");
         if (can_propagate()) {
-            generate_induction_lemmas(get_context());
             propagate();
             return FC_CONTINUE;
         }