--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Thu Mar 05 13:28:04 2015 +0100
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Fri Mar 06 00:00:57 2015 +0100
@@ -108,15 +108,13 @@
fun match_instantiateT ctxt t thm =
if Term.exists_type (Term.exists_subtype Term.is_TVar) (dest_thm thm) then
- let val certT = Proof_Context.ctyp_of ctxt
- in Thm.instantiate (gen_certify_inst fst TVar certT ctxt thm t, []) thm end
+ Thm.instantiate (gen_certify_inst fst TVar (Proof_Context.ctyp_of ctxt) ctxt thm t, []) thm
else thm
fun match_instantiate ctxt t thm =
- let
- val cert = Proof_Context.cterm_of ctxt
- val thm' = match_instantiateT ctxt t thm
- in Thm.instantiate ([], gen_certify_inst snd Var cert ctxt thm' t) thm' end
+ let val thm' = match_instantiateT ctxt t thm in
+ Thm.instantiate ([], gen_certify_inst snd Var (Proof_Context.cterm_of ctxt) ctxt thm' t) thm'
+ end
fun apply_rule ctxt t =
(case Z3_Replay_Rules.apply ctxt (certify_prop ctxt t) of