1 files changed, 5 insertions, 4 deletions
diff --git a/src/theory/shared_terms_database.h b/src/theory/shared_terms_database.h
index ddb1a4043..3b21c27a8 100644
--- a/src/theory/shared_terms_database.h
+++ b/src/theory/shared_terms_database.h
@@ -32,6 +32,7 @@
 
 namespace cvc5 {
 
+class Env;
 class TheoryEngine;
 
 class SharedTermsDatabase : public context::ContextNotifyObj {
@@ -43,6 +44,9 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
   typedef shared_terms_list::const_iterator shared_terms_iterator;
 
  private:
+  /** Reference to the env */
+  Env& d_env;
+
   /** Some statistics */
   IntStat d_statSharedTerms;
 
@@ -158,10 +162,7 @@ class SharedTermsDatabase : public context::ContextNotifyObj {
    * @param pnm The proof node manager to use, which is non-null if proofs
    * are enabled.
    */
-  SharedTermsDatabase(TheoryEngine* theoryEngine,
-                      context::Context* context,
-                      context::UserContext* userContext,
-                      ProofNodeManager* pnm);
+  SharedTermsDatabase(Env& env, TheoryEngine* theoryEngine);
 
   //-------------------------------------------- initialization
   /** Called to set the equality engine. */