# HG changeset patch
# User paulson
# Date 1175702705 -7200
# Node ID de39593f2948f8d30effb34241f02a8756430207
# Parent  97b5290a8c348470be9b6d4a3b941973e63c26c3
find_first is just an alias

diff -r 97b5290a8c34 -r de39593f2948 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