dest_select : term -> term * term
STRUCTURE
SYNOPSIS
Breaks apart a choice term into selected variable and body.
DESCRIPTION
If M has the form @v. t then dest_select M returns (v,t).
FAILURE
Fails if M is not an epsilon-term.
SEEALSO
HOL  Trindemossen-1