dest_comb : term -> term * term
STRUCTURE
SYNOPSIS
Breaks apart a combination (function application) into rator and rand.
DESCRIPTION
dest_comb is a term destructor for combinations. If term M has the form f x, then dest_comb M equals (f,x).
FAILURE
Fails if the argument is not a function application.
SEEALSO
HOL  Kananaskis-13