2 files changed, 0 insertions, 42 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 3313a684f..15891dfad 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -289,9 +289,6 @@ constant BUILTIN \
     "expr/kind.h" \
     "the kind of expressions representing built-in operators"
 
-variable FUNCTION "a defined function"
-parameterized APPLY FUNCTION 0: "application of a defined function"
-
 operator EQUAL 2 "equality (two parameters only, sorts must match)"
 operator DISTINCT 2: "disequality (N-ary, sorts must match)"
 variable VARIABLE "a variable (not permitted in bindings)"
@@ -332,7 +329,6 @@ well-founded SEXPR_TYPE \
     "::CVC4::theory::builtin::SExprProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 
-typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 2c726d12f..db427d21e 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -31,44 +31,6 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-class ApplyTypeRule {
- public:
-  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
-  {
-    TNode f = n.getOperator();
-    TypeNode fType = f.getType(check);
-    if( !fType.isFunction() && n.getNumChildren() > 0 ) {
-      throw TypeCheckingExceptionPrivate(n, "operator does not have function type");
-    }
-    if( check ) {
-      if(fType.isFunction()) {
-        if(n.getNumChildren() != fType.getNumChildren() - 1) {
-          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
-        }
-        TNode::iterator argument_it = n.begin();
-        TNode::iterator argument_it_end = n.end();
-        TypeNode::iterator argument_type_it = fType.begin();
-        for(; argument_it != argument_it_end; ++argument_it, ++argument_type_it) {
-          if(!(*argument_it).getType().isComparableTo(*argument_type_it)) {
-            std::stringstream ss;
-            ss << "argument types do not match the function type:\n"
-               << "argument:  " << *argument_it << "\n"
-               << "has type:  " << (*argument_it).getType() << "\n"
-               << "not equal: " << *argument_type_it;
-            throw TypeCheckingExceptionPrivate(n, ss.str());
-          }
-        }
-      } else {
-        if( n.getNumChildren() > 0 ) {
-          throw TypeCheckingExceptionPrivate(n, "number of arguments does not match the function type");
-        }
-      }
-    }
-    return fType.isFunction() ? fType.getRangeType() : fType;
-  }
-};/* class ApplyTypeRule */
-
-
 class EqualityTypeRule {
  public:
   inline static TypeNode computeType(NodeManager* nodeManager,