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

SYNOPSIS
Applies a binary destructor repeatedly in right-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:
  rev_splitlist d f(...(f(f(w,x1),x2),...xn)
returns
  (w,[x1; ... ; xn])

FAILURE CONDITIONS
Never fails.

EXAMPLE
The function strip_comb is actually just defined as rev_splitlist dest_comb, which acts as follows:
  # rev_splitlist dest_comb `x + 1 + 2`;;
  val it : term * term list = (`(+)`, [`x`; `1 + 2`])

SEE ALSO
itlist, nsplit, splitlist, striplist.