----------------------------------------------------------------------
strip_binder                                                    (Term)
----------------------------------------------------------------------
strip_binder : term option -> term -> term list * term

SYNOPSIS
Break apart consecutive binders.

KEYWORDS
variable, binding.

DESCRIBE
An application {strip_binder (SOME c) (c(\v1. ... (c(\vn.M))...))}
returns {([v1,...,vn],M)}. The constant {c} should represent a term
binding operation.

An application {strip_binder NONE (\v1...vn. M)} returns {([v1,...,vn],M)}.

FAILURE
Never fails.

EXAMPLE
{strip_abs} could be defined as follows.

   - val strip_abs = strip_binder NONE;
   > val strip_abs = fn : term -> term list * term

   - strip_abs (Term `\x y z. x /\ y ==> z`);
   > val it = ([`x`, `y`, `z`], `x /\ y ==> z`) : term list * term

Defining {strip_forall} is similar.

   strip_binder (SOME boolSyntax.universal)




COMMENTS
Terms with many consecutive binders should be taken apart using
{strip_binder} and its instantiations {strip_abs}, {strip_forall},
and {strip_exists}. In the current implementation of HOL, iterating
{dest_abs}, {dest_forall}, or {dest_exists} is far slower for terms
with many consecutive binders.

SEEALSO
Term.list_mk_binder, Term.strip_abs, boolSyntax.strip_forall,
boolSyntax.strip_exists.

----------------------------------------------------------------------