# HG changeset patch
# User wenzelm
# Date 1199200166 -3600
# Node ID 374446e935589841d88e098cfbb5fcd9bfdc8ccb
# Parent  a4e69ce247e0d5e748816bfcb2b098b74ea76aa4
removed separate exists/forall code;

diff -r a4e69ce247e0 -r 374446e93558 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jan 01 07:28:20 2008 +0100
+++ b/src/Pure/library.ML	Tue Jan 01 16:09:26 2008 +0100
@@ -315,17 +315,8 @@
 fun p orf q = fn x => p x orelse q x;
 fun p andf q = fn x => p x andalso q x;
 
-(*exists pred [x1, ..., xn] ===> pred x1 orelse ... orelse pred xn*)
-fun exists (pred: 'a -> bool) : 'a list -> bool =
-  let fun boolf [] = false
-        | boolf (x :: xs) = pred x orelse boolf xs
-  in boolf end;
-
-(*forall pred [x1, ..., xn] ===> pred x1 andalso ... andalso pred xn*)
-fun forall (pred: 'a -> bool) : 'a list -> bool =
-  let fun boolf [] = true
-        | boolf (x :: xs) = pred x andalso boolf xs
-  in boolf end;
+val exists = List.exists;
+val forall = List.all;
 
 
 (* flags *)