2 files changed, 18 insertions, 37 deletions
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index f6540b9da..2f2c77d36 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -4,9 +4,22 @@
 # src/expr/builtin_kinds.
 #
 
-operator PLUS "arithmetic addition"
-operator MULT "arithmetic multiplication"
-operator UMINUS "arithmetic negation"
+theory ::CVC4::theory::arith::TheoryArith "theory_arith.h"
 
-constant CONST_RATIONAL ::CVC4::Rational "a multiple-precision rational constant"
-constant CONST_INTEGER ::CVC4::Integer "a multiple-precision integer constant"
+operator PLUS 2: "arithmetic addition"
+operator MULT 2: "arithmetic multiplication"
+operator UMINUS 1 "arithmetic negation"
+
+constant \
+    CONST_RATIONAL \
+    ::CVC4::Rational \
+    ::CVC4::RationalHashFcn \
+    "util/rational.h" \
+    "a multiple-precision rational constant"
+
+constant \
+    CONST_INTEGER \
+    ::CVC4::Integer \
+    ::CVC4::IntegerHashFcn \
+    "util/integer.h" \
+    "a multiple-precision integer constant"
diff --git a/src/theory/arith/theory_def.h b/src/theory/arith/theory_def.h
deleted file mode 100644
index da4239724..000000000
--- a/src/theory/arith/theory_def.h
+++ /dev/null
@@ -1,32 +0,0 @@
-/*********************                                                        */
-/** theory_def.h
- ** Original author: mdeters
- ** Major contributors: none
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.
- **
- ** Definition for TheoryARITH (for purposes of linking to the
- ** theory-code-finding mechanisms in the parent directory).
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__ARITH__THEORY_DEF_H
-#define __CVC4__THEORY__ARITH__THEORY_DEF_H
-
-#include "theory/arith/theory_arith.h"
-
-namespace CVC4 {
-  namespace theory {
-    namespace arith {
-      typedef TheoryArith TheoryARITH;
-    }
-  }
-}
-
-#endif /* __CVC4__THEORY__ARITH__THEORY_DEF_H */