----------------------------------------------------------------------
strip_disj                                                (boolSyntax)
----------------------------------------------------------------------
strip_disj : term -> term list

SYNOPSIS
Recursively breaks apart disjunctions.

DESCRIBE
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
boolSyntax.dest_disj, boolSyntax.mk_disj, boolSyntax.list_mk_disj.

----------------------------------------------------------------------