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