If M is a term of the form \v1...vn.N, where N is not a lambda abstraction,
then strip_abs M equals ([v1,...,vn],N). Otherwise, the result
is ([],M).
FAILURE
Never fails.
EXAMPLE
- strip_abs (Term `\x y z. x ==> y ==> z`);
> val it = ([`x`, `y`, `z`], `x ==> y ==> z`) : term list * term
- strip_abs T;
> val it = ([], `T`) : term list * term
COMMENTS
In the current implementation of HOL, strip_abs is far faster
than iterating dest_abs for terms with many consecutive binders.