--- 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;
--- 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)
}