type_vars_in_term : term -> hol_type list
STRUCTURE
Term
SYNOPSIS
Return the type variables occurring in a term.
DESCRIPTION
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 = [`:'b`, `:'a`] : hol_type list

SEEALSO
free_vars, type_vars
HOL  Trindemossen-1