# HG changeset patch
# User wenzelm
# Date 1121786510 -7200
# Node ID 07213f0e291f2ae508740f79ee63864ef5c0e174
# Parent  e92cba1d4842125a9267027f6c1c4508930eccd2
added has_duplicates;
tuned qsort;

diff -r e92cba1d4842 -r 07213f0e291f src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jul 19 17:21:49 2005 +0200
+++ b/src/Pure/library.ML	Tue Jul 19 17:21:50 2005 +0200
@@ -209,6 +209,7 @@
   val findrep: ''a list -> ''a list
   val gen_duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val duplicates: ''a list -> ''a list
+  val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
 
   (*association lists*)
   val assoc: (''a * 'b) list * ''a -> 'b option
@@ -638,7 +639,7 @@
 exception UnequalLengths;
 
 fun map2 _ ([], []) = []
-  | map2 f (x :: xs, y :: ys) = (f (x, y) :: map2 f (xs, ys))
+  | map2 f (x :: xs, y :: ys) = f (x, y) :: map2 f (xs, ys)
   | map2 _ _ = raise UnequalLengths;
 
 fun exists2 _ ([], []) = false
@@ -983,7 +984,6 @@
 
 fun distinct l = gen_distinct (op =) l;
 
-
 (*returns the tail beginning with the first repeated element, or []*)
 fun findrep [] = []
   | findrep (x :: xs) = if x mem xs then x :: xs else findrep xs;
@@ -1006,6 +1006,12 @@
 
 fun duplicates l = gen_duplicates (op =) l;
 
+fun has_duplicates eq =
+  let
+    fun dups [] = false
+      | dups (x :: xs) = member eq xs x orelse dups xs;
+  in dups end;
+
 
 
 (** association lists **)
@@ -1154,14 +1160,12 @@
 (*quicksort (stable, i.e. does not reorder equal elements)*)
 fun sort ord =
   let
-    fun qsort xs =
-      let val len = length xs in
-        if len <= 1 then xs
-        else
-          let val (lts, eqs, gts) = part (nth_elem (len div 2, xs)) xs in
-            qsort lts @ eqs @ qsort gts
-          end
-      end
+    fun qsort [] = []
+      | qsort (xs as [_]) = xs
+      | qsort (xs as [x, y]) = if ord (x, y) = GREATER then [y, x] else xs
+      | qsort xs =
+          let val (lts, eqs, gts) = part (nth_elem (length xs div 2, xs)) xs
+          in qsort lts @ eqs @ qsort gts end
     and part _ [] = ([], [], [])
       | part pivot (x :: xs) = add (ord (x, pivot)) x (part pivot xs)
     and add LESS x (lts, eqs, gts) = (x :: lts, eqs, gts)