free_varsl
Term.free_varsl : term list -> term list
Returns the set of free variables in a list of terms.
An invocation free_varsl [t1,...,tn] returns a list representing the
set of free term variables occurring in t1,...,tn.
Failure
Never fails.
Example
> free_varsl [Term `x /\ y /\ y ==> x`,
Term `!x. x ==> p ==> y`];
val it = [“x”, “y”, “p”]: term list
Comments
Code should not depend on how elements are arranged in the result of
free_varsl.
free_varsl 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_vars,
Term.empty_varset,
Type.type_vars