5 files changed, 28 insertions, 7 deletions
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index 48fe4d84a..c4c3435a2 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -298,6 +298,8 @@ variable BOUND_VARIABLE "bound variable"
 variable SKOLEM "skolem var"
 operator TUPLE 1: "a tuple"
 
+operator LAMBDA 2 "lambda"
+
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
     ::CVC4::TypeConstantHashFunction \
@@ -338,6 +340,7 @@ typerule APPLY ::CVC4::theory::builtin::ApplyTypeRule
 typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
 typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
 typerule TUPLE ::CVC4::theory::builtin::TupleTypeRule
+typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
 
 constant SUBTYPE_TYPE \
     ::CVC4::Predicate \
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index 68d9e8702..95ede1c46 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -145,6 +145,24 @@ public:
   }
 };/* class StringConstantTypeRule */
 
+class LambdaTypeRule {
+public:
+  inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+    if( n[0].getType(check) != nodeManager->boundVarListType() ) {
+      std::stringstream ss;
+      ss << "expected a bound var list for LAMBDA expression, got `"
+         << n[0].getType().toString() << "'";
+      throw TypeCheckingExceptionPrivate(n, ss.str());
+    }
+    std::vector<TypeNode> argTypes;
+    for(TNode::iterator i = n[0].begin(); i != n[0].end(); ++i) {
+      argTypes.push_back((*i).getType());
+    }
+    TypeNode rangeType = n[1].getType(check);
+    return nodeManager->mkFunctionType(argTypes, rangeType);
+  }
+};/* class LambdaTypeRule */
+
 class SortProperties {
 public:
   inline static bool isWellFounded(TypeNode type) {
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index e928010b6..b0728de29 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -473,7 +473,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
         for( int i=0; i<(int)body[0].getNumChildren(); i++ ){
           //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){
           terms.push_back( body[0][i] );
-          subs.push_back( NodeManager::currentNM()->mkSkolem( body[0][i].getType() ) );
+          subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
         }
         args.insert( args.end(), subs.begin(), subs.end() );
       }else{
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index cc74e3e76..a73d42a31 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -14,11 +14,11 @@
  ** \brief Implementation of term databse class
  **/
 
- #include "theory/quantifiers/term_database.h"
- #include "theory/quantifiers_engine.h"
- #include "theory/uf/theory_uf_instantiator.h"
- #include "theory/theory_engine.h"
- #include "theory/quantifiers/first_order_model.h"
+#include "theory/quantifiers/term_database.h"
+#include "theory/quantifiers_engine.h"
+#include "theory/uf/theory_uf_instantiator.h"
+#include "theory/theory_engine.h"
+#include "theory/quantifiers/first_order_model.h"
 
 using namespace std;
 using namespace CVC4;
diff --git a/src/theory/rewriterules/theory_rewriterules_type_rules.h b/src/theory/rewriterules/theory_rewriterules_type_rules.h
index 605324b20..f03fba73a 100644
--- a/src/theory/rewriterules/theory_rewriterules_type_rules.h
+++ b/src/theory/rewriterules/theory_rewriterules_type_rules.h
@@ -60,7 +60,7 @@ public:
     }
     return nodeManager->booleanType();
   }
-};/* class RewriterulesTypeRule */
+};/* class RewriteRuleTypeRule */
 
 
 class RRRewriteTypeRule {