1.1 --- a/src/HOL/Library/reflection.ML	Sat Oct 17 21:14:08 2009 +0200
     1.2 +++ b/src/HOL/Library/reflection.ML	Sat Oct 17 22:34:19 2009 +0200
     1.3 @@ -79,12 +79,6 @@
     1.4  
     1.5  fun dest_listT (Type (@{type_name "list"}, [T])) = T;
     1.6  
     1.7 -(* This modified version of divide_and_conquer allows the threading
     1.8 -   of a state variable *)
     1.9 -fun divide_and_conquer' decomp s x =
    1.10 -  let val ((ys, recomb), s') = decomp s x
    1.11 -  in recomb (fold_map (divide_and_conquer' decomp) ys s') end;
    1.12 -
    1.13  fun rearrange congs =
    1.14    let
    1.15      fun P (_, th) =

     2.1 --- a/src/Pure/library.ML	Sat Oct 17 21:14:08 2009 +0200
     2.2 +++ b/src/Pure/library.ML	Sat Oct 17 22:34:19 2009 +0200
     2.3 @@ -217,6 +217,8 @@
     2.4  
     2.5    (*misc*)
     2.6    val divide_and_conquer: ('a -> 'a list * ('b list -> 'b)) -> 'a -> 'b
     2.7 +  val divide_and_conquer': ('a -> 'b -> ('a list * ('c list * 'b -> 'c * 'b)) * 'b) ->
     2.8 +    'a -> 'b -> 'c * 'b
     2.9    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
    2.10    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
    2.11    val gensym: string -> string
    2.12 @@ -1067,6 +1069,10 @@
    2.13    let val (ys, recomb) = decomp x
    2.14    in recomb (map (divide_and_conquer decomp) ys) end;
    2.15  
    2.16 +fun divide_and_conquer' decomp x s =
    2.17 +  let val ((ys, recomb), s') = decomp x s
    2.18 +  in recomb (fold_map (divide_and_conquer' decomp) ys s') end;
    2.19 +
    2.20  
    2.21  (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
    2.22     putting x in bk if p(k)(x) holds.  Preserve order of elements if possible.*)