changeset 59590 | 7ade9a33c653 |
parent 59586 | ddf6deaadfe8 |
child 59621 | 291934bac95e |
--- a/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Wed Mar 04 22:56:25 2015 +0100 +++ b/src/HOL/Library/Old_SMT/old_z3_proof_tools.ML Wed Mar 04 23:14:38 2015 +0100 @@ -156,7 +156,7 @@ | NONE => let val (n, ctxt') = yield_singleton Variable.variant_fixes "x" ctxt - val cv = Old_SMT_Utils.certify ctxt' + val cv = Proof_Context.cterm_of ctxt' (Free (n, map Thm.typ_of_cterm cvs' ---> Thm.typ_of_cterm ct)) val cu = Drule.list_comb (cv, cvs') val e = (t, (cv, fold_rev Thm.lambda cvs' ct))