--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Mar 06 23:54:05 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML Fri Mar 06 23:54:36 2015 +0100
@@ -566,20 +566,18 @@
might be needed (not the whole "Thm.prop_of scheme_thm")*)
fun diff_and_instantiate ctxt scheme_thm scheme_t instance_t =
let
- val thy = Proof_Context.theory_of ctxt
-
val (term_pairing, type_pairing) =
- diff thy (scheme_t, instance_t)
+ diff (Proof_Context.theory_of ctxt) (scheme_t, instance_t)
(*valuation of type variables*)
- val typeval = map (apply2 (Thm.global_ctyp_of thy)) type_pairing
+ val typeval = map (apply2 (Thm.ctyp_of ctxt)) type_pairing
val typeval_env =
map (apfst dest_TVar) type_pairing
(*valuation of term variables*)
val termval =
map (apfst (type_devar typeval_env)) term_pairing
- |> map (apply2 (Thm.global_cterm_of thy))
+ |> map (apply2 (Thm.cterm_of ctxt))
in
Thm.instantiate (typeval, termval) scheme_thm
end
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 06 23:54:05 2015 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Fri Mar 06 23:54:36 2015 +0100
@@ -806,8 +806,6 @@
ML {*
fun instantiate_skols ctxt consts_candidates i = fn st =>
let
- val thy = Proof_Context.theory_of ctxt
-
val gls =
Thm.prop_of st
|> Logic.strip_horn
@@ -917,7 +915,7 @@
(* val contextualise = fold absdummy (map snd params) *)
val contextualise = fold absfree params
- val skolem_cts = map (contextualise #> Thm.global_cterm_of thy) skolem_terms
+ val skolem_cts = map (contextualise #> Thm.cterm_of ctxt) skolem_terms
(*now the instantiation code*)
@@ -937,7 +935,7 @@
fun make_var pre_var =
the_single pre_var
|> Var
- |> Thm.global_cterm_of thy
+ |> Thm.cterm_of ctxt
|> SOME
in
if null pre_var then NONE
@@ -2003,7 +2001,7 @@
thy
prob_name (#meta pannot) n
|> the
- |> (fn {inference_fmla, ...} => Thm.global_cterm_of thy inference_fmla)
+ |> (fn {inference_fmla, ...} => Thm.cterm_of ctxt inference_fmla)
|> oracle_iinterp
end
*}