# HG changeset patch
# User wenzelm
# Date 1709999528 -3600
# Node ID d71af537a6e960895b4668eb60c1a7570a87fa30
# Parent  2a3c0a68221cc7a3e761b0196a5be80e38b043f0
obsolete;

diff -r 2a3c0a68221c -r d71af537a6e9 src/Pure/library.scala
--- a/src/Pure/library.scala	Sat Mar 09 16:50:54 2024 +0100
+++ b/src/Pure/library.scala	Sat Mar 09 16:52:08 2024 +0100
@@ -284,9 +284,6 @@
       case _ => error(message)
     }
 
-  def symmetric_difference[A](xs: List[A], ys: List[A]): (List[A], List[A]) =
-    (xs.filterNot(ys.toSet), ys.filterNot(xs.toSet))
-
 
   /* proper values */