src/HOL/TPTP/TPTP_Parser/tptp_reconstruct_library.ML

 
     val (term_pairing, type_pairing) =
       diff thy (scheme_t, instance_t)
 
     (*valuation of type variables*)
-    val typeval = map (apply2 (Thm.ctyp_of thy)) type_pairing
+    val typeval = map (apply2 (Thm.global_ctyp_of thy)) 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.cterm_of thy))
+      |> map (apply2 (Thm.global_cterm_of thy))
   in
     Thm.instantiate (typeval, termval) scheme_thm
   end
 
 (*FIXME this is bad form?*)