dest_pabs
pairSyntax.dest_pabs : term -> term * term
Breaks apart a paired abstraction into abstracted pair and body.
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.
See also
Term.dest_abs,
pairSyntax.mk_pabs,
pairSyntax.is_pabs,
pairSyntax.strip_pabs