# HG changeset patch
# User wenzelm
# Date 1476466345 -7200
# Node ID ad15c2f478b51cf417c0360f4701eea5a3084e1b
# Parent  cb98e0e5f1e58f6df7c47401c2101413f86ed9ff
more general operations;

diff -r cb98e0e5f1e5 -r ad15c2f478b5 src/Pure/library.scala
--- a/src/Pure/library.scala	Fri Oct 14 19:08:13 2016 +0200
+++ b/src/Pure/library.scala	Fri Oct 14 19:32:25 2016 +0200
@@ -204,21 +204,21 @@
     else if (xs.isEmpty) ys
     else ys.foldRight(xs)(Library.insert(_)(_))
 
-  def distinct[A](xs: List[A]): List[A] =
+  def distinct[A](xs: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
   {
     val result = new mutable.ListBuffer[A]
-    xs.foreach(x => if (!result.contains(x)) result += x)
+    xs.foreach(x => if (!result.exists(y => eq(x, y))) result += x)
     result.toList
   }
 
-  def duplicates[A](lst: List[A]): List[A] =
+  def duplicates[A](lst: List[A], eq: (A, A) => Boolean = (x: A, y: A) => x == y): List[A] =
   {
     val result = new mutable.ListBuffer[A]
     @tailrec def dups(rest: List[A]): Unit =
       rest match {
         case Nil =>
         case x :: xs =>
-          if (!result.contains(x) && xs.contains(x)) result += x
+          if (!result.exists(y => eq(x, y)) && xs.exists(y => eq(x, y))) result += x
           dups(xs)
       }
     dups(lst)