1 files changed, 3 insertions, 4 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h
index 450bd7991..8fff7eafe 100644
--- a/src/theory/quantifiers/conjecture_generator.h
+++ b/src/theory/quantifiers/conjecture_generator.h
@@ -18,6 +18,7 @@
 #define CONJECTURE_GENERATOR_H
 
 #include "context/cdhashmap.h"
+#include "expr/node_trie.h"
 #include "theory/quantifiers_engine.h"
 #include "theory/type_enumerator.h"
 
@@ -25,8 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace quantifiers {
 
-class TermArgTrie;
-
 //algorithm for computing candidate subgoals
 
 class ConjectureGenerator;
@@ -105,8 +104,8 @@ class TermGenerator
   //2 : variables must map to non-ground terms
   unsigned d_match_mode;
   //children
-  std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children;
-  std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end;
+  std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children;
+  std::vector<std::map<TNode, TNodeTrie>::iterator> d_match_children_end;
 
   void reset( TermGenEnv * s, TypeNode tn );
   bool getNextTerm( TermGenEnv * s, unsigned depth );