src/Pure/library.ML
changeset 22593 de39593f2948
parent 22582 f315da9400fb
child 23202 98736a2fec98
     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