diff -r b8920f3fd259 -r 89ccf66aa73d src/HOL/Tools/SMT/z3_proof_methods.ML
--- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Feb 15 23:19:30 2012 +0100
@@ -109,7 +109,7 @@
       SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt
     val (cl, cv) = Thm.dest_binop ct
     val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
-    val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
+    val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf))
   in Thm.assume (SMT_Utils.mk_cequals cg cu) end
 
 fun prove_inj_eq ctxt ct =