free_varsl : term list -> term list
STRUCTURE
Term
SYNOPSIS
Returns the set of free variables in a list of terms.
DESCRIPTION
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.

SEEALSO
FVL, free_vars_lr, free_vars, empty_varset, type_vars
HOL  Trindemossen-1