Breaks apart an application of a given binary operator to two arguments.
DESCRIPTION
The call dest_binop op t, where t is of the form (op l) r, will return
the pair l,r. If t is not of that form, it fails. Note that op can be any
term; it need not be a constant nor parsed infix.
FAILURE CONDITIONS
Fails if the term is not a binary application of operator op.
EXAMPLE
# dest_binop `(+):num->num->num` `1 + 2 + 3`;;
val it : term * term = (`1`, `2 + 3`)