diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
index 91f5b68ec..013c3c188 100644
--- a/src/smt/theory_array_full.cpp
+++ b/src/smt/theory_array_full.cpp
@@ -35,6 +35,10 @@ namespace smt {
         m_var_data_full.reset();
     }
 
+    theory* theory_array_full::mk_fresh(context* new_ctx) { 
+        return alloc(theory_array_full, new_ctx->get_manager(), m_params); 
+    }
+
     void theory_array_full::add_map(theory_var v, enode* s) {
         if (m_params.m_array_cg && !s->is_cgr()) {
             return;
diff --git a/src/smt/theory_array_full.h b/src/smt/theory_array_full.h
index 730c325dc..1200275a2 100644
--- a/src/smt/theory_array_full.h
+++ b/src/smt/theory_array_full.h
@@ -91,7 +91,7 @@ namespace smt {
         theory_array_full(ast_manager & m, theory_array_params & params);
         virtual ~theory_array_full();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_array_full, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual void merge_eh(theory_var v1, theory_var v2, theory_var, theory_var);
         virtual void display_var(std::ostream & out, theory_var v) const;
diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp
index a004da666..cf4658c7d 100644
--- a/src/smt/theory_datatype.cpp
+++ b/src/smt/theory_datatype.cpp
@@ -36,6 +36,11 @@ namespace smt {
         virtual theory_id get_from_theory() const { return null_theory_id; } 
     };
 
+
+    theory* theory_datatype::mk_fresh(context* new_ctx) { 
+        return alloc(theory_datatype, new_ctx->get_manager(), m_params); 
+    }
+
     /**
        \brief Assert the axiom (antecedent => lhs = rhs)
        antecedent may be null_literal
diff --git a/src/smt/theory_datatype.h b/src/smt/theory_datatype.h
index 99511665f..77b1ffc7c 100644
--- a/src/smt/theory_datatype.h
+++ b/src/smt/theory_datatype.h
@@ -101,7 +101,7 @@ namespace smt {
     public:
         theory_datatype(ast_manager & m, theory_datatype_params & p);
         virtual ~theory_datatype();
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_datatype, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
         virtual void display(std::ostream & out) const;
         virtual void collect_statistics(::statistics & st) const;        
         virtual void init_model(model_generator & m);
diff --git a/src/smt/theory_dense_diff_logic.h b/src/smt/theory_dense_diff_logic.h
index cc739c8bc..1b1653eb7 100644
--- a/src/smt/theory_dense_diff_logic.h
+++ b/src/smt/theory_dense_diff_logic.h
@@ -282,7 +282,7 @@ namespace smt {
         theory_dense_diff_logic(ast_manager & m, theory_arith_params & p);
         virtual ~theory_dense_diff_logic() { reset_eh(); }
         
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_dense_diff_logic, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "difference-logic"; }
 
diff --git a/src/smt/theory_dense_diff_logic_def.h b/src/smt/theory_dense_diff_logic_def.h
index 4c35647e8..7702a1ef2 100644
--- a/src/smt/theory_dense_diff_logic_def.h
+++ b/src/smt/theory_dense_diff_logic_def.h
@@ -39,6 +39,11 @@ namespace smt {
         m_edges.push_back(edge());
     }
 
+    template<typename Ext>
+    theory* theory_dense_diff_logic<Ext>::mk_fresh(context * new_ctx) { 
+        return alloc(theory_dense_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
+    }
+
     template<typename Ext>
     inline app * theory_dense_diff_logic<Ext>::mk_zero_for(expr * n) {
         return m_autil.mk_numeral(rational(0), get_manager().get_sort(n));
diff --git a/src/smt/theory_diff_logic.h b/src/smt/theory_diff_logic.h
index 84735a411..390bd271d 100644
--- a/src/smt/theory_diff_logic.h
+++ b/src/smt/theory_diff_logic.h
@@ -243,7 +243,7 @@ namespace smt {
             reset_eh();
         }
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_diff_logic, new_ctx->get_manager(), m_params); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "difference-logic"; }
 
diff --git a/src/smt/theory_diff_logic_def.h b/src/smt/theory_diff_logic_def.h
index c791668c3..f444fe88e 100644
--- a/src/smt/theory_diff_logic_def.h
+++ b/src/smt/theory_diff_logic_def.h
@@ -1384,5 +1384,11 @@ bool theory_diff_logic<Ext>::internalize_objective(expr * n, rational const& m,
     return true;
 }
 
+template<typename Ext>
+theory* theory_diff_logic<Ext>::mk_fresh(context* new_ctx) {
+    return alloc(theory_diff_logic<Ext>, new_ctx->get_manager(), m_params); 
+}
+
+
 #endif /* THEORY_DIFF_LOGIC_DEF_H_ */
 
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 66a1a6321..8b031ff27 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -716,6 +716,10 @@ namespace smt {
         return;
     }
 
+    theory* theory_fpa::mk_fresh(context* new_ctx) { 
+        return alloc(theory_fpa, new_ctx->get_manager()); 
+    }
+
     void theory_fpa::push_scope_eh() {
         theory::push_scope_eh();
         m_trail_stack.push_scope();
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index a62c35cd2..9db6a88a9 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -158,7 +158,7 @@ namespace smt {
         virtual void push_scope_eh();
         virtual void pop_scope_eh(unsigned num_scopes);
         virtual void reset_eh();
-        virtual theory* mk_fresh(context* new_ctx) { return alloc(theory_fpa, new_ctx->get_manager()); }
+        virtual theory* mk_fresh(context* new_ctx);
         virtual char const * get_name() const { return "fpa"; }
 
         virtual model_value_proc * mk_value(enode * n, model_generator & mg);
diff --git a/src/smt/theory_utvpi.cpp b/src/smt/theory_utvpi.cpp
index c45cfe74a..9da82c9e6 100644
--- a/src/smt/theory_utvpi.cpp
+++ b/src/smt/theory_utvpi.cpp
@@ -156,5 +156,5 @@ namespace smt {
         return true;
     }
 
-
+    
 }
diff --git a/src/smt/theory_utvpi.h b/src/smt/theory_utvpi.h
index daba28045..35ebd440b 100644
--- a/src/smt/theory_utvpi.h
+++ b/src/smt/theory_utvpi.h
@@ -183,7 +183,7 @@ namespace smt {
 
         virtual ~theory_utvpi();
 
-        virtual theory * mk_fresh(context * new_ctx) { return alloc(theory_utvpi, new_ctx->get_manager()); }
+        virtual theory * mk_fresh(context * new_ctx);
 
         virtual char const * get_name() const { return "utvpi-logic"; }
 
diff --git a/src/smt/theory_utvpi_def.h b/src/smt/theory_utvpi_def.h
index bca24406f..22b19b0b1 100644
--- a/src/smt/theory_utvpi_def.h
+++ b/src/smt/theory_utvpi_def.h
@@ -942,6 +942,10 @@ namespace smt {
         }
     }
 
+    template<typename Ext>
+    theory* theory_utvpi<Ext>::mk_fresh(context* new_ctx) { 
+        return alloc(theory_utvpi<Ext>, new_ctx->get_manager()); 
+    }
 
 
 };