dest_select : term -> term * term
STRUCTURE
boolSyntax
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
mk_select
,
is_select
HOL
Kananaskis-14