src/Pure/thm.ML

   val generalize: string list * string list -> int -> thm -> thm
   val instantiate: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
   val trivial: cterm -> thm
   val class_triv: theory -> class -> thm
   val unconstrainT: ctyp -> thm -> thm
-  val varifyT: thm -> thm
-  val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val dest_state: thm * int -> (term * term) list * term list * term * term
   val lift_rule: cterm -> thm -> thm
   val incr_indexes: int -> thm -> thm
   val assumption: int -> thm -> thm Seq.seq
   val eq_assumption: int -> thm -> thm

   val adjust_maxidx_thm: thm -> thm
   val rename_boundvars: term -> term -> thm -> thm
   val cterm_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   val cterm_first_order_match: cterm * cterm -> (ctyp * ctyp) list * (cterm * cterm) list
   val cterm_incr_indexes: int -> cterm -> cterm
+  val varifyT: thm -> thm
+  val varifyT': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm
   val freezeT: thm -> thm
 end;
 
 structure Thm: THM =
 struct