# HG changeset patch
# User wenzelm
# Date 1425682476 -3600
# Node ID f596ed64701857ec161c00edb99602fd5ca0b640
# Parent  cb84e420fc8e77e731c36370debf9b1e8df39d75
clarified context;

diff -r cb84e420fc8e -r f596ed647018 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML
--- 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
diff -r cb84e420fc8e -r f596ed647018 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- 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
 *}