# HG changeset patch
# User wenzelm
# Date 1148161022 -7200
# Node ID dd9ccb370f521aeaf0cbe648eb6159981d86b13a
# Parent  8c03cadf98861d4c125a82fd28c93916e2939e3a
removed obsolete partition (cf. List.partition);
tuned;

diff -r 8c03cadf9886 -r dd9ccb370f52 src/Pure/library.ML
--- a/src/Pure/library.ML	Sat May 20 23:37:00 2006 +0200
+++ b/src/Pure/library.ML	Sat May 20 23:37:02 2006 +0200
@@ -288,7 +288,6 @@
   val drop: int * 'a list -> 'a list
   val last_elem: 'a list -> 'a
   val seq: ('a -> unit) -> 'a list -> unit
-  val partition: ('a -> bool) -> 'a list -> 'a list * 'a list
 end;
 
 structure Library: LIBRARY =
@@ -1228,18 +1227,6 @@
   let val (ys, recomb) = decomp x
   in recomb (map (divide_and_conquer decomp) ys) end;
 
-(*Partition list into elements that satisfy predicate and those that don't.
-  Preserves order of elements in both lists.*)
-val partition = List.partition;
-
-fun partition_eq (eq:'a * 'a -> bool) =
-  let
-    fun part [] = []
-      | part (x :: ys) =
-          let val (xs, xs') = partition (fn y => eq (x, y)) ys
-          in (x::xs)::(part xs') end
-  in part 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.*)
@@ -1249,10 +1236,19 @@
               (case xs of [] => []
                          | _ => raise Fail "partition_list")
             else
-            let val (ns, rest) = partition (p k) xs;
+            let val (ns, rest) = List.partition (p k) xs;
             in  ns :: part(k+1)rest  end
   in  part i end;
 
+fun partition_eq (eq:'a * 'a -> bool) =
+  let
+    fun part [] = []
+      | part (x :: ys) =
+          let val (xs, xs') = List.partition (fn y => eq (x, y)) ys
+          in (x::xs)::(part xs') end
+  in part end;
+
+
 
 (* generating identifiers *)