diff --git a/src/model/char_factory.h b/src/model/char_factory.h
index 55baad26d..ca7632816 100644
--- a/src/model/char_factory.h
+++ b/src/model/char_factory.h
@@ -21,7 +21,6 @@ Revision History:
 #include "model/value_factory.h"
 
 class char_factory final : public value_factory {
-    model_core&  m_model;
     seq_util     u;
     uint_set     m_chars;
     unsigned     m_next { 'A' };
@@ -29,9 +28,8 @@ class char_factory final : public value_factory {
 
 public:
     
-    char_factory(ast_manager & m, family_id fid, model_core& md):
+    char_factory(ast_manager & m, family_id fid):
         value_factory(m, fid),
-        m_model(md),
         u(m),
         m_trail(m)
     {
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 9b618a2c5..6338b58ff 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -24,7 +24,6 @@ Notes:
 
 #include <queue>
 #include <fstream>
-#include <functional>
 #include <algorithm>
 
 #include "util/scoped_ptr_vector.h"
@@ -188,7 +187,7 @@ public:
     }
 };
 
- struct lemma_lt_proc : public std::function<bool(lemma*, lemma *)> {
+struct lemma_lt_proc {
     bool operator() (lemma *a, lemma *b) {
         return (a->level () < b->level ()) ||
             (a->level () == b->level () &&
@@ -731,11 +730,11 @@ inline std::ostream &operator<<(std::ostream &out, pob const &p) {
     return p.display(out);
 }
 
- struct pob_lt_proc : public std::function<bool(const pob*, const pob*)> {
+struct pob_lt_proc {
     bool operator() (const pob *pn1, const pob *pn2) const;
 };
 
- struct pob_gt_proc : public std::function<bool(const pob*, const pob*)> {
+struct pob_gt_proc {
     bool operator() (const pob *n1, const pob *n2) const {
         return pob_lt_proc()(n2, n1);
     }
diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp
index 651871e5a..5a2e9d362 100644
--- a/src/muz/spacer/spacer_quant_generalizer.cpp
+++ b/src/muz/spacer/spacer_quant_generalizer.cpp
@@ -36,7 +36,7 @@ Revision History:
 using namespace spacer;
 
 namespace {
-    struct index_lt_proc : public std::function<bool(app*, app *)> {
+struct index_lt_proc {
     arith_util m_arith;
     index_lt_proc(ast_manager &m) : m_arith(m) {}
     bool operator() (app *a, app *b) {
diff --git a/src/smt/theory_char.cpp b/src/smt/theory_char.cpp
index f32f99714..f1fb4f05d 100644
--- a/src/smt/theory_char.cpp
+++ b/src/smt/theory_char.cpp
@@ -376,7 +376,7 @@ namespace smt {
 
     // a stand-alone theory.
     void theory_char::init_model(model_generator & mg) {
-        m_factory = alloc(char_factory, get_manager(), get_family_id(), mg.get_model());
+        m_factory = alloc(char_factory, get_manager(), get_family_id());
         mg.register_factory(m_factory);
         for (auto val : m_var2value) 
             if (val != UINT_MAX)