src/Pure/type.ML

   val freeze_thaw: term -> term * (term -> term)
   val freeze: term -> term
 
   (*matching and unification*)
   exception TYPE_MATCH
-  type tyenv
+  type tyenv = (sort * typ) Vartab.table
   val lookup: tyenv * (indexname * sort) -> typ option
   val typ_match: tsig -> typ * typ -> tyenv -> tyenv
   val typ_instance: tsig -> typ * typ -> bool
   val raw_match: typ * typ -> tyenv -> tyenv
   val raw_matches: typ list * typ list -> tyenv -> tyenv