Fix assertion.

diff --git a/src/theory/datatypes/datatypes_rewriter.h b/src/theory/datatypes/datatypes_rewriter.h
index 8214f23e2c7ff28108e8abe2da5530cb634af2d5..c8ce9833c61980961b69a7c2dac1659cdb41acb2 100644 (file)
--- a/src/theory/datatypes/datatypes_rewriter.h
+++ b/src/theory/datatypes/datatypes_rewriter.h
@@ -320,7 +320,7 @@ public:
     return false;
   }
   static bool isNullaryApplyConstructor( Node n ){
-    Assert( n.getKind()==APPLY_CONSTRUCTOR );
+    Assert( n.getKind()==kind::APPLY_CONSTRUCTOR );
     for( unsigned i=0; i<n.getNumChildren(); i++ ){
       if( n[i].getType().isDatatype() ){
         return false;