type_vars_in_term
Term.type_vars_in_term : term -> hol_type list
Return the type variables occurring in a term.
An invocation type_vars_in_term M returns the set of type variables
occurring in M.
Failure
Never fails.
Example
> type_vars_in_term (concl boolTheory.ONE_ONE_DEF);
val it = [“:β”, “:α”]: hol_type list