dest_pabs : term -> term * term
STRUCTURE
LIBRARY
pair
SYNOPSIS
Breaks apart a paired abstraction into abstracted pair and body.
DESCRIPTION
dest_pabs is a term destructor for paired abstractions: dest_abs "\pair. t" returns ("pair","t").
FAILURE
Fails with dest_pabs if term is not a paired abstraction.
SEEALSO
HOL  Kananaskis-13