--- a/src/Pure/library.ML Sat Oct 17 21:14:08 2009 +0200
+++ b/src/Pure/library.ML Sat Oct 17 22:34:19 2009 +0200
@@ -217,6 +217,8 @@
(*misc*)
val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
+ val divide_and_conquer': ('a -> 'b -> ('a list * ('c list * 'b -> 'c * 'b)) * 'b) ->
+ 'a -> 'b -> 'c * 'b
val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
val gensym: string -> string
@@ -1067,6 +1069,10 @@
let val (ys, recomb) = decomp x
in recomb (map (divide_and_conquer decomp) ys) end;
+fun divide_and_conquer' decomp x s =
+ let val ((ys, recomb), s') = decomp x s
+ in recomb (fold_map (divide_and_conquer' decomp) ys s') end;
+
(*Partition a list into buckets [ bi, b(i+1), ..., bj ]
putting x in bk if p(k)(x) holds. Preserve order of elements if possible.*)