strip_comb : term -> term * term list
STRUCTURE
boolSyntax
SYNOPSIS
Iteratively breaks apart combinations (function applications).
DESCRIPTION
If M has the form t t1 ... tn then strip_comb M returns (t,[t1,...,tn]). Note that 
   strip_comb(list_mk_comb(t,[t1,...,tn]))
will not be (t,[t1,...,tn]) if t is a combination.
FAILURE
Never fails.
EXAMPLE
- strip_comb (Term `x /\ y`);
> val it = (`$/\`, [`x`, `y`]) : term * term list

- strip_comb T;
> val it = (`T`, []) : term * term list

SEEALSO
list_mk_comb, dest_comb
HOL  Kananaskis-13