src/HOL/Tools/SMT/z3_proof_methods.ML
changeset 46497 89ccf66aa73d
parent 45392 828e08541cee
child 51717 9e7d1c139569
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_methods.ML	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4        SMT_Utils.dest_all_cbinders (SMT_Utils.dest_cprop rhs) ctxt
     1.5      val (cl, cv) = Thm.dest_binop ct
     1.6      val (cg, (cargs, cf)) = Drule.strip_comb cl ||> split_last
     1.7 -    val cu = fold_rev Thm.cabs cargs (mk_inv_of ctxt' (Thm.cabs cv cf))
     1.8 +    val cu = fold_rev Thm.lambda cargs (mk_inv_of ctxt' (Thm.lambda cv cf))
     1.9    in Thm.assume (SMT_Utils.mk_cequals cg cu) end
    1.10  
    1.11  fun prove_inj_eq ctxt ct =