# HG changeset patch
# User wenzelm
# Date 1255811659 -7200
# Node ID a473ba9a221dc484d26ec8eda370e0dfc8490881
# Parent  d83b9ad78d4bad9e4af244fde09a3a3f7f19eec4
tuned/moved divide_and_conquer';

diff -r d83b9ad78d4b -r a473ba9a221d src/HOL/Library/reflection.ML
--- a/src/HOL/Library/reflection.ML	Sat Oct 17 21:14:08 2009 +0200
+++ b/src/HOL/Library/reflection.ML	Sat Oct 17 22:34:19 2009 +0200
@@ -79,12 +79,6 @@
 
 fun dest_listT (Type (@{type_name "list"}, [T])) = T;
 
-(* This modified version of divide_and_conquer allows the threading
-   of a state variable *)
-fun divide_and_conquer' decomp s x =
-  let val ((ys, recomb), s') = decomp s x
-  in recomb (fold_map (divide_and_conquer' decomp) ys s') end;
-
 fun rearrange congs =
   let
     fun P (_, th) =
diff -r d83b9ad78d4b -r a473ba9a221d src/Pure/library.ML
--- 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.*)