removed obsolete partition (cf. List.partition);
authorwenzelm
Sat May 20 23:37:02 2006 +0200 (2006-05-20)
changeset 19691dd9ccb370f52
parent 19690 8c03cadf9886
child 19692 bad13b32c0f3
removed obsolete partition (cf. List.partition);
tuned;
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Sat May 20 23:37:00 2006 +0200
     1.2 +++ b/src/Pure/library.ML	Sat May 20 23:37:02 2006 +0200
     1.3 @@ -288,7 +288,6 @@
     1.4    val drop: int * 'a list -> 'a list
     1.5    val last_elem: 'a list -> 'a
     1.6    val seq: ('a -> unit) -> 'a list -> unit
     1.7 -  val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
     1.8  end;
     1.9  
    1.10  structure Library: LIBRARY =
    1.11 @@ -1228,18 +1227,6 @@
    1.12    let val (ys, recomb) = decomp x
    1.13    in recomb (map (divide_and_conquer decomp) ys) end;
    1.14  
    1.15 -(*Partition list into elements that satisfy predicate and those that don't.
    1.16 -  Preserves order of elements in both lists.*)
    1.17 -val partition = List.partition;
    1.18 -
    1.19 -fun partition_eq (eq:'a * 'a -> bool) =
    1.20 -  let
    1.21 -    fun part [] = []
    1.22 -      | part (x :: ys) =
    1.23 -          let val (xs, xs') = partition (fn y => eq (x, y)) ys
    1.24 -          in (x::xs)::(part xs') end
    1.25 -  in part end;
    1.26 -
    1.27  
    1.28  (*Partition a list into buckets  [ bi, b(i+1), ..., bj ]
    1.29     putting x in bk if p(k)(x) holds.  Preserve order of elements if possible.*)
    1.30 @@ -1249,10 +1236,19 @@
    1.31                (case xs of [] => []
    1.32                           | _ => raise Fail "partition_list")
    1.33              else
    1.34 -            let val (ns, rest) = partition (p k) xs;
    1.35 +            let val (ns, rest) = List.partition (p k) xs;
    1.36              in  ns :: part(k+1)rest  end
    1.37    in  part i end;
    1.38  
    1.39 +fun partition_eq (eq:'a * 'a -> bool) =
    1.40 +  let
    1.41 +    fun part [] = []
    1.42 +      | part (x :: ys) =
    1.43 +          let val (xs, xs') = List.partition (fn y => eq (x, y)) ys
    1.44 +          in (x::xs)::(part xs') end
    1.45 +  in part end;
    1.46 +
    1.47 +
    1.48  
    1.49  (* generating identifiers *)
    1.50