dest_disj : term -> term * term
STRUCTURE
SYNOPSIS
Term destructor for disjunctions.
DESCRIPTION
If M is a term having the form t1 \/ t2, then dest_disj M returns (t1,t2).
FAILURE
Fails if M is not a disjunction.
SEEALSO
HOL  Trindemossen-1