find_first is just an alias
authorpaulson
Wed Apr 04 18:05:05 2007 +0200 (2007-04-04)
changeset 22593de39593f2948
parent 22592 97b5290a8c34
child 22594 33a690455f88
find_first is just an alias
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Wed Apr 04 00:13:13 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Apr 04 18:05:05 2007 +0200
     1.3 @@ -509,9 +509,7 @@
     1.4  fun find_index_eq x = find_index (equal x);
     1.5  
     1.6  (*find first element satisfying predicate*)
     1.7 -fun find_first _ [] = NONE
     1.8 -  | find_first pred (x :: xs) =
     1.9 -      if pred x then SOME x else find_first pred xs;
    1.10 +val find_first = List.find;
    1.11  
    1.12  (*get first element by lookup function*)
    1.13  fun get_first _ [] = NONE