author | paulson |
Wed, 04 Apr 2007 18:05:05 +0200 | |
changeset 22593 | de39593f2948 |
parent 22592 | 97b5290a8c34 |
child 22594 | 33a690455f88 |
--- 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