src/HOL/Tools/ATP/atp_util.ML

   val nat_subscript : int -> string
   val unyxml : string -> string
   val maybe_quote : string -> string
   val string_from_ext_time : bool * Time.time -> string
   val string_from_time : Time.time -> string
-  val type_instance : Proof.context -> typ -> typ -> bool
-  val type_generalization : Proof.context -> typ -> typ -> bool
-  val type_intersect : Proof.context -> typ -> typ -> bool
-  val type_equiv : Proof.context -> typ * typ -> bool
+  val type_instance : theory -> typ -> typ -> bool
+  val type_generalization : theory -> typ -> typ -> bool
+  val type_intersect : theory -> typ -> typ -> bool
+  val type_equiv : theory -> typ * typ -> bool
   val varify_type : Proof.context -> typ -> typ
   val instantiate_type : theory -> typ -> typ -> typ -> typ
   val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
   val typ_of_dtyp : Datatype.descr -> (Datatype.dtyp * typ) list -> Datatype.dtyp -> typ
   val is_type_surely_finite : Proof.context -> typ -> bool

        string_of_real (0.01 * Real.fromInt (ms div 10)) ^ " s")
   end
 
 val string_from_time = string_from_ext_time o pair false
 
-fun type_instance ctxt T T' =
-  Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
-fun type_generalization ctxt T T' = type_instance ctxt T' T
-fun type_intersect ctxt T T' =
-  can (Sign.typ_unify (Proof_Context.theory_of ctxt)
-                      (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
+fun type_instance thy T T' = Sign.typ_instance thy (T, T')
+fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
+fun type_intersect thy T T' =
+  can (Sign.typ_unify thy (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
       (Vartab.empty, 0)
-val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
+val type_equiv = Sign.typ_equiv
 
 fun varify_type ctxt T =
   Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
   |> snd |> the_single |> dest_Const |> snd
 

     val thy = Proof_Context.theory_of ctxt
     val max = 2 (* 1 would be too small for the "fun" case *)
     fun aux slack avoid T =
       if member (op =) avoid T then
         0
-      else case AList.lookup (type_equiv ctxt) assigns T of
+      else case AList.lookup (type_equiv thy) assigns T of
         SOME k => k
       | NONE =>
         case T of
           Type (@{type_name fun}, [T1, T2]) =>
           (case (aux slack avoid T1, aux slack avoid T2) of