src/Pure/library.ML

--- a/src/Pure/library.ML	Wed Apr 04 00:13:13 2007 +0200
+++ b/src/Pure/library.ML	Wed Apr 04 18:05:05 2007 +0200
@@ -509,9 +509,7 @@
 fun find_index_eq x = find_index (equal x);
 
 (*find first element satisfying predicate*)
-fun find_first _ [] = NONE
-  | find_first pred (x :: xs) =
-      if pred x then SOME x else find_first pred xs;
+val find_first = List.find;
 
 (*get first element by lookup function*)
 fun get_first _ [] = NONE