# HG changeset patch
# User wenzelm
# Date 1139338608 -3600
# Node ID dc49d8b188863b07abc2c01af48aa842a8241bfb
# Parent  3b76383e3ab3aaee8b146524cb95a5ab0bc94e53
removed eq-polymorphic duplicates;
renamed gen_duplicates to duplicates;
added is_equal;

diff -r 3b76383e3ab3 -r dc49d8b18886 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Feb 07 19:56:47 2006 +0100
+++ b/src/Pure/library.ML	Tue Feb 07 19:56:48 2006 +0100
@@ -214,8 +214,7 @@
   val gen_distinct: ('a * 'a -> bool) -> 'a list -> 'a list
   val distinct: ''a list -> ''a list
   val findrep: ''a list -> ''a list
-  val gen_duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
-  val duplicates: ''a list -> ''a list
+  val duplicates: ('a * 'a -> bool) -> 'a list -> 'a list
   val has_duplicates: ('a * 'a -> bool) -> 'a list -> bool
 
   (*lists as tables -- see also Pure/General/alist.ML*)
@@ -233,6 +232,7 @@
   val accesses_bal: ('a -> 'a) * ('a -> 'a) * 'a -> int -> 'a list
 
   (*orders*)
+  val is_equal: order -> bool
   val rev_order: order -> order
   val make_ord: ('a * 'a -> bool) -> 'a * 'a -> order
   val eq_ord: ('a -> order) -> 'a -> bool
@@ -1025,18 +1025,14 @@
 
 (*returns a list containing all repeated elements exactly once; preserves
   order, takes first of equal elements*)
-fun gen_duplicates eq lst =
+fun duplicates eq lst =
   let
     fun dups (rev_dups, []) = rev rev_dups
       | dups (rev_dups, x :: xs) =
           if member eq rev_dups x orelse not (member eq xs x) then
             dups (rev_dups, xs)
           else dups (x :: rev_dups, xs);
-  in
-    dups ([], lst)
-  end;
-
-fun duplicates l = gen_duplicates (op =) l;
+  in dups ([], lst) end;
 
 fun has_duplicates eq =
   let
@@ -1100,6 +1096,9 @@
 
 (** orders **)
 
+fun is_equal EQUAL = true
+  | is_equal _ = false;
+
 fun rev_order LESS = GREATER
   | rev_order EQUAL = EQUAL
   | rev_order GREATER = LESS;