free_vars
Term.free_vars : term -> term list
Returns the set of free variables in a term.
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.
See also
Term.FVL, Term.free_vars_lr,
Term.free_varsl,
Term.empty_varset,
Type.type_vars