Returns a list of the variables free in a theorem's assumptions and conclusion.
DESCRIPTION
When applied to a theorem, A |- t, the function thm_frees returns a list,
without repetitions, of those variables which are free either in t or in
some member of the assumption list A.
FAILURE CONDITIONS
Never fails.
EXAMPLE
# let th = CONJUNCT1 (ASSUME `p /\ q`);;
val th : thm = p /\ q |- p
# thm_frees th;;
val it : term list = [`q`; `p`]