strip_disj : term -> term list
STRUCTURE
SYNOPSIS
Recursively breaks apart disjunctions.
DESCRIPTION
If M is of the form t1 \/ ... \/ tn, where no ti is a disjunction, then strip_disj M returns [t1,...,tn]. Any ti that is a disjunction is broken down by strip_disj, hence
   strip_disj(list_mk_disj [t1,...,tn])
will not return [t1,...,tn] if any ti is a disjunction.
FAILURE
Never fails.
EXAMPLE
- strip_disj (Term `(a \/ b) \/ c \/ d`);
> val it = [`a`, `b`, `c`, `d`] : term list

SEEALSO
HOL  Trindemossen-1