freesl : term list -> term list

SYNOPSIS
Returns a list of the free variables in a list of terms.

DESCRIPTION
When applied to a list of terms, freesl returns a list of the variables which are free in any of those terms. There are no repetitions in the list produced even if several terms contain the same free variable.

FAILURE CONDITIONS
Never fails.

EXAMPLE
In the following example there are free instances of each of w, x and y, whereas the only instances of z are bound:
  # freesl [`x + y = 2`; `!z. z >= x - w`];;
  val it : term list = [`y`; `x`; `w`]

SEE ALSO
frees, free_in, thm_frees.