1 files changed, 13 insertions, 75 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5cf19aab9..99db9feb2 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -808,37 +808,37 @@ class NodeManager {
                            const typename AttrKind::value_type& value);
 
   /** Get the (singleton) type for Booleans. */
-  inline TypeNode booleanType();
+  TypeNode booleanType();
 
   /** Get the (singleton) type for integers. */
-  inline TypeNode integerType();
+  TypeNode integerType();
 
   /** Get the (singleton) type for reals. */
-  inline TypeNode realType();
+  TypeNode realType();
 
   /** Get the (singleton) type for strings. */
-  inline TypeNode stringType();
+  TypeNode stringType();
 
   /** Get the (singleton) type for RegExp. */
-  inline TypeNode regExpType();
+  TypeNode regExpType();
 
   /** Get the (singleton) type for rounding modes. */
-  inline TypeNode roundingModeType();
+  TypeNode roundingModeType();
 
   /** Get the bound var list type. */
-  inline TypeNode boundVarListType();
+  TypeNode boundVarListType();
 
   /** Get the instantiation pattern type. */
-  inline TypeNode instPatternType();
+  TypeNode instPatternType();
 
   /** Get the instantiation pattern type. */
-  inline TypeNode instPatternListType();
+  TypeNode instPatternListType();
 
   /**
    * Get the (singleton) type for builtin operators (that is, the type
    * of the Node returned from Node::getOperator() when the operator
    * is built-in, like EQUAL). */
-  inline TypeNode builtinOperatorType();
+  TypeNode builtinOperatorType();
 
   /**
    * Make a function type from domain to range.
@@ -906,11 +906,11 @@ class NodeManager {
 
   /** Make the type of floating-point with <code>exp</code> bit exponent and
       <code>sig</code> bit significand */
-  inline TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
-  inline TypeNode mkFloatingPointType(FloatingPointSize fs);
+  TypeNode mkFloatingPointType(unsigned exp, unsigned sig);
+  TypeNode mkFloatingPointType(FloatingPointSize fs);
 
   /** Make the type of bitvectors of size <code>size</code> */
-  inline TypeNode mkBitVectorType(unsigned size);
+  TypeNode mkBitVectorType(unsigned size);
 
   /** Make the type of arrays with the given parameterization */
   inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
@@ -1129,56 +1129,6 @@ public:
   }
 };/* class NodeManagerScope */
 
-/** Get the (singleton) type for booleans. */
-inline TypeNode NodeManager::booleanType() {
-  return TypeNode(mkTypeConst<TypeConstant>(BOOLEAN_TYPE));
-}
-
-/** Get the (singleton) type for integers. */
-inline TypeNode NodeManager::integerType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INTEGER_TYPE));
-}
-
-/** Get the (singleton) type for reals. */
-inline TypeNode NodeManager::realType() {
-  return TypeNode(mkTypeConst<TypeConstant>(REAL_TYPE));
-}
-
-/** Get the (singleton) type for strings. */
-inline TypeNode NodeManager::stringType() {
-  return TypeNode(mkTypeConst<TypeConstant>(STRING_TYPE));
-}
-
-/** Get the (singleton) type for regexps. */
-inline TypeNode NodeManager::regExpType() {
-  return TypeNode(mkTypeConst<TypeConstant>(REGEXP_TYPE));
-}
-
-/** Get the (singleton) type for rounding modes. */
-inline TypeNode NodeManager::roundingModeType() {
-  return TypeNode(mkTypeConst<TypeConstant>(ROUNDINGMODE_TYPE));
-}
-
-/** Get the bound var list type. */
-inline TypeNode NodeManager::boundVarListType() {
-  return TypeNode(mkTypeConst<TypeConstant>(BOUND_VAR_LIST_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_TYPE));
-}
-
-/** Get the instantiation pattern type. */
-inline TypeNode NodeManager::instPatternListType() {
-  return TypeNode(mkTypeConst<TypeConstant>(INST_PATTERN_LIST_TYPE));
-}
-
-/** Get the (singleton) type for builtin operators. */
-inline TypeNode NodeManager::builtinOperatorType() {
-  return TypeNode(mkTypeConst<TypeConstant>(BUILTIN_OPERATOR_TYPE));
-}
-
 inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
   std::vector<TypeNode> typeNodes;
   for (unsigned i = 0; i < types.size(); ++ i) {
@@ -1187,18 +1137,6 @@ inline TypeNode NodeManager::mkSExprType(const std::vector<TypeNode>& types) {
   return mkTypeNode(kind::SEXPR_TYPE, typeNodes);
 }
 
-inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
-  return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
-}
-
-inline TypeNode NodeManager::mkFloatingPointType(unsigned exp, unsigned sig) {
-  return TypeNode(mkTypeConst<FloatingPointSize>(FloatingPointSize(exp,sig)));
-}
-
-inline TypeNode NodeManager::mkFloatingPointType(FloatingPointSize fs) {
-  return TypeNode(mkTypeConst<FloatingPointSize>(fs));
-}
-
 inline TypeNode NodeManager::mkArrayType(TypeNode indexType,
                                          TypeNode constituentType) {
   CheckArgument(!indexType.isNull(), indexType,