splitlist : ('a -> 'b * 'a) -> 'a -> 'b list * 'a

SYNOPSIS
Applies a binary destructor repeatedly in left-associative mode.

DESCRIPTION
If a destructor function d inverts a binary constructor f, for example dest_comb for mk_comb, and fails when applied to y, then:
  splitlist d (f(x1,f(x2,f(...f(xn,y)))))
returns
  ([x1; ... ; xn],y)

FAILURE CONDITIONS
Never fails.

EXAMPLE
The function strip_forall is actually just defined as splitlist dest_forall, which acts as follows:
  # splitlist dest_forall `!x y z. x + y = z`;;
  val it : term list * term = ([`x`; `y`; `z`], `x + y = z`)

SEE ALSO
itlist, nsplit, rev_splitlist, striplist.