dest_gabs : term -> term * term

SYNOPSIS
Breaks apart a generalized abstraction into abstracted varstruct and body.

DESCRIPTION
dest_pabs is a term destructor for generalized abstractions: for example with a paired varstruct the effect on dest_pabs `\(v1..(..)..vn). t` is to return the pair (`(v1..(..)..vn)`,`t`). It will also act as for dest_abs on basic abstractions.

FAILURE CONDITIONS
Fails unless the term is a basic or generalized abstraction.

EXAMPLE
These are fairly typical applications:
  # dest_gabs `\(x,y). x + y`;;
  val it : term * term = (`x,y`, `x + y`)

  # dest_gabs `\(CONS h t). h + 1`;;
  val it : term * term = (`CONS h t`, `h + 1`)
while the following shows that it also works on basic abstractions:
  # dest_gabs `\x. x`;;
  Warning: inventing type variables
  val it : term * term = (`x`, `x`)

SEE ALSO
GEN_BETA_CONV, is_gabs, mk_gabs, strip_gabs.