all_vars : term -> term list

- STRUCTURE
- 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

HOL Kananaskis-14