src/HOL/TPTP/TPTP_Proof_Reconstruction.thy

 *}
 
 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
       |> fst
 

 
     (*prefix a skolem term with bindings for the parameters*)
     (* 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*)
 
     (*there should only be one Var -- that is from the previous application of drule leo2_skolemise. We look for it at the head position in some equation at a conclusion of a subgoal.*)

           |> maps (switch Term.add_vars [])
 
         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
         else make_var pre_var
      end

   in
     TPTP_Reconstruct.inference_at_node
      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
 *}