Breaks apart an instance of a binary operator with given name.
DESCRIPTION
The call dest_binary s tm will, if tm is a binary operator application
(op l) r where op is a constant with name s, return the two arguments to
which it is applied as a pair l,r. Otherwise, it fails. Note that op is
required to be a constant.
FAILURE CONDITIONS
Never fails.
EXAMPLE
This one succeeds:
# dest_binary "+" `1 + 2`;;
val it : term * term = (`1`, `2`)