This is the datatype for the intermediate representation of HOL types. It includes an extra class for "generated tyvars", used in term parsing and printing as a temporary placeholder for an as-yet-undetermined type (whereas "conventional tyvars" come from user annotations and internal types and are fixed for the purposes of parsing and printing). Generated tyvars have a number attribute. This is by default '0', which imparts no information, but gets assigned a unique non-zero value during preterm detyping (see 'TypeAnal' module).