all_vars : term -> term list
STRUCTURE
Term
SYNOPSIS
Returns the set of all variables in a term.
DESCRIPTION
An invocation all_vars ty returns a list representing the set of all bound and free term variables occurring in tm.
FAILURE
Never fails.
EXAMPLE
- all_vars (Term `!x y. x /\ y /\ y ==> z`);
> val it = [`z`, `y`, `x`] : term list

COMMENTS
Code should not depend on how elements are arranged in the result of all_vars.
SEEALSO
free_vars, all_varsl
HOL  Kananaskis-8