all_vars : term -> term list
STRUCTURE
Term
SYNOPSIS
Returns the set of all variables in a term.
DESCRIPTION
An invocation all_vars tm returns a list representing the set of all bound and free term variables occurring in tm.
FAILURE
Never fails.
EXAMPLE
- all_vars ``!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
all_atoms, all_varsl, free_vars
HOL  Kananaskis-13