# HG changeset patch
# User wenzelm
# Date 1418337723 -3600
# Node ID fd748d770770b495a1c3e089078f950ae67bc3a8
# Parent  c2b23cb8a6778d58783251c265dc746111aa47b1
tuned;

diff -r c2b23cb8a677 -r fd748d770770 src/Pure/Concurrent/par_list.ML
--- a/src/Pure/Concurrent/par_list.ML	Thu Dec 11 23:31:30 2014 +0100
+++ b/src/Pure/Concurrent/par_list.ML	Thu Dec 11 23:42:03 2014 +0100
@@ -68,8 +68,7 @@
 
 fun find_some P = get_some (fn x => if P x then SOME x else NONE);
 
-fun exists P = is_some o get_some (fn x => if P x then SOME () else NONE);
-
+fun exists P = is_some o find_some P;
 fun forall P = not o exists (not o P);
 
 end;
diff -r c2b23cb8a677 -r fd748d770770 src/Pure/Concurrent/par_list.scala
--- a/src/Pure/Concurrent/par_list.scala	Thu Dec 11 23:31:30 2014 +0100
+++ b/src/Pure/Concurrent/par_list.scala	Thu Dec 11 23:42:03 2014 +0100
@@ -62,9 +62,7 @@
   def find_some[A](P: A => Boolean, xs: List[A]): Option[A] =
     get_some((x: A) => if (P(x)) Some(x) else None, xs)
 
-  def exists[A](P: A => Boolean, xs: List[A]): Boolean =
-    get_some((x: A) => if (P(x)) Some(()) else None, xs).isDefined
-
+  def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined
   def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs)
 }