From a2d69183485f9c96fd5fc813e69354438be89ff1 Mon Sep 17 00:00:00 2001
From: Soonho Kong <soonhok@cs.cmu.edu>
Date: Sun, 1 Dec 2013 22:22:56 -0500
Subject: [PATCH] fix(library/rewriter): use Abst axiom in lambda_body RW

---
 src/library/rewriter/rewriter.cpp       | 5 +----
 src/tests/library/rewriter/rewriter.cpp | 3 +--
 2 files changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/library/rewriter/rewriter.cpp b/src/library/rewriter/rewriter.cpp
index 772f039df..023148efb 100644
--- a/src/library/rewriter/rewriter.cpp
+++ b/src/library/rewriter/rewriter.cpp
@@ -92,10 +92,7 @@ pair<expr, expr> rewrite_lambda_body(environment const & env, context & ctx, exp
         expr const & new_v   = mk_lambda(n, ty, new_body);
         expr const & ty_body = ti(body, extend(ctx, n, ty));
         lean_assert_eq(ty_body, ti(new_body, ctx)); // TODO(soonhok): generalize for hetreogeneous types
-        expr const & proof   = Subst(ty_body, body, new_body,
-                                     Fun({Const("e"), ty_body},
-                                         mk_eq(v, mk_lambda(n, ty, Const("e")))),
-                                     Refl(ty_v, v), pf_body);
+        expr const & proof = Abst(ty, mk_lambda(n, ty, ty_body), v, new_v, mk_lambda(n, ty, pf_body));
         return make_pair(new_v, proof);
     }
 }
diff --git a/src/tests/library/rewriter/rewriter.cpp b/src/tests/library/rewriter/rewriter.cpp
index c489d6118..5c13888e6 100644
--- a/src/tests/library/rewriter/rewriter.cpp
+++ b/src/tests/library/rewriter/rewriter.cpp
@@ -725,8 +725,7 @@ static void lambda_rewriter2_tst() {
     cout << "Concl = " << concl << std::endl
          << "Proof = " << proof << std::endl;
     lean_assert_eq(concl, mk_eq(v, mk_lambda("x", Nat, nAdd(a, Var(0)))));
-    // TODO(soonhok): this one doesn't work now.
-//    env.add_theorem("lambda_rewriter2", concl, proof);
+    env.add_theorem("lambda_rewriter2", concl, proof);
     cout << "====================================================" << std::endl;
 }