1.1 --- a/src/HOL/Tools/ATP/atp_util.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/ATP/atp_util.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -16,10 +16,10 @@
     1.4    val maybe_quote : string -> string
     1.5    val string_from_ext_time : bool * Time.time -> string
     1.6    val string_from_time : Time.time -> string
     1.7 -  val type_instance : Proof.context -> typ -> typ -> bool
     1.8 -  val type_generalization : Proof.context -> typ -> typ -> bool
     1.9 -  val type_intersect : Proof.context -> typ -> typ -> bool
    1.10 -  val type_equiv : Proof.context -> typ * typ -> bool
    1.11 +  val type_instance : theory -> typ -> typ -> bool
    1.12 +  val type_generalization : theory -> typ -> typ -> bool
    1.13 +  val type_intersect : theory -> typ -> typ -> bool
    1.14 +  val type_equiv : theory -> typ * typ -> bool
    1.15    val varify_type : Proof.context -> typ -> typ
    1.16    val instantiate_type : theory -> typ -> typ -> typ -> typ
    1.17    val varify_and_instantiate_type : Proof.context -> typ -> typ -> typ -> typ
    1.18 @@ -123,14 +123,12 @@
    1.19  
    1.20  val string_from_time = string_from_ext_time o pair false
    1.21  
    1.22 -fun type_instance ctxt T T' =
    1.23 -  Sign.typ_instance (Proof_Context.theory_of ctxt) (T, T')
    1.24 -fun type_generalization ctxt T T' = type_instance ctxt T' T
    1.25 -fun type_intersect ctxt T T' =
    1.26 -  can (Sign.typ_unify (Proof_Context.theory_of ctxt)
    1.27 -                      (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
    1.28 +fun type_instance thy T T' = Sign.typ_instance thy (T, T')
    1.29 +fun type_generalization thy T T' = Sign.typ_instance thy (T', T)
    1.30 +fun type_intersect thy T T' =
    1.31 +  can (Sign.typ_unify thy (T, Logic.incr_tvar (maxidx_of_typ T + 1) T'))
    1.32        (Vartab.empty, 0)
    1.33 -val type_equiv = Sign.typ_equiv o Proof_Context.theory_of
    1.34 +val type_equiv = Sign.typ_equiv
    1.35  
    1.36  fun varify_type ctxt T =
    1.37    Variable.polymorphic_types ctxt [Const (@{const_name undefined}, T)]
    1.38 @@ -177,7 +175,7 @@
    1.39      fun aux slack avoid T =
    1.40        if member (op =) avoid T then
    1.41          0
    1.42 -      else case AList.lookup (type_equiv ctxt) assigns T of
    1.43 +      else case AList.lookup (type_equiv thy) assigns T of
    1.44          SOME k => k
    1.45        | NONE =>
    1.46          case T of