dest_res_abstract : term -> (term # term # term)
STRUCTURE
SYNOPSIS
Breaks apart a restricted abstract term into the quantified variable, predicate and body.
DESCRIPTION
dest_res_abstract is a term destructor for restricted abstraction:
   dest_res_abstract "\var::P. t"
returns ("var","P","t").
FAILURE
Fails with dest_res_abstract if the term is not a restricted abstraction.
SEEALSO
HOL  Trindemossen-1