1.1 --- a/src/Pure/thm.ML	Sun Apr 25 22:50:47 2010 +0200
     1.2 +++ b/src/Pure/thm.ML	Sun Apr 25 23:09:32 2010 +0200
     1.3 @@ -92,8 +92,6 @@
     1.4    val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
     1.5    val instantiate_cterm: (ctyp * ctyp) list * (cterm * cterm) list -> cterm -> cterm
     1.6    val trivial: cterm -> thm
     1.7 -  val of_class: ctyp * class -> thm
     1.8 -  val unconstrainT: ctyp -> thm -> thm
     1.9    val dest_state: thm * int -> (term * term) list * term list * term * term
    1.10    val lift_rule: cterm -> thm -> thm
    1.11    val incr_indexes: int -> thm -> thm
    1.12 @@ -139,6 +137,9 @@
    1.13    val adjust_maxidx_thm: int -> thm -> thm
    1.14    val varifyT_global: thm -> thm
    1.15    val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
    1.16 +  val of_class: ctyp * class -> thm
    1.17 +  val unconstrainT: ctyp -> thm -> thm
    1.18 +  val unconstrain_allTs: thm -> thm
    1.19    val freezeT: thm -> thm
    1.20    val assumption: int -> thm -> thm Seq.seq
    1.21    val eq_assumption: int -> thm -> thm
    1.22 @@ -1240,6 +1241,11 @@
    1.23        prop = Logic.list_implies (constraints, unconstrain prop)})
    1.24    end;
    1.25  
    1.26 +fun unconstrain_allTs th =
    1.27 +  fold (unconstrainT o ctyp_of (theory_of_thm th) o TVar)
    1.28 +    (fold_terms Term.add_tvars th []) th;
    1.29 +
    1.30 +
    1.31  (* Replace all TFrees not fixed or in the hyps by new TVars *)
    1.32  fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
    1.33    let