frees : term -> term list

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

DESCRIPTION
When applied to a term, frees returns a list of the free variables in that term. There are no repetitions in the list produced even if there are multiple free instances of some variables.

FAILURE CONDITIONS
Never fails.

EXAMPLE
Clearly in the following term, x and y are free, whereas z is bound:
  # frees `x = 1 /\ y = 2 /\ !z. z >= 0`;;
  val it : term list = [`x`; `y`]

SEE ALSO
freesl, free_in, thm_frees, variables.