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

COMMENTS
Code should not depend on how elements are arranged in the result of free_vars.

free_vars is not efficient for large terms with many free variables. Demanding applications should be coded with FVL.

SEEALSO
FVL, free_vars_lr, free_varsl, empty_varset, type_vars
HOL  Kananaskis-13