2 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp
index b808f4cd5..86fc057ea 100644
--- a/src/theory/quantifiers/theory_quantifiers.cpp
+++ b/src/theory/quantifiers/theory_quantifiers.cpp
@@ -34,8 +34,8 @@ using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
 
-TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, SmtGlobals* globals) :
-    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo, globals),
+TheoryQuantifiers::TheoryQuantifiers(Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+    Theory(THEORY_QUANTIFIERS, c, u, out, valuation, logicInfo),
   d_masterEqualityEngine(0)
 {
   d_numInstantiations = 0;
diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h
index 63f3379b8..6335349b1 100644
--- a/src/theory/quantifiers/theory_quantifiers.h
+++ b/src/theory/quantifiers/theory_quantifiers.h
@@ -53,7 +53,7 @@ private:
 public:
   TheoryQuantifiers(context::Context* c, context::UserContext* u,
                     OutputChannel& out, Valuation valuation,
-                    const LogicInfo& logicInfo, SmtGlobals* globals);
+                    const LogicInfo& logicInfo);
   ~TheoryQuantifiers();
 
   void setMasterEqualityEngine(eq::EqualityEngine* eq);