# HG changeset patch # User ballarin # Date 1229014551 -3600 # Node ID c2a750c8a37b4572e86ba9198664e1d61167c587 # Parent b0c81b9a013359b9b76df6a4c62531262abf0cf4 Clarified comment. diff -r b0c81b9a0133 -r c2a750c8a37b src/Pure/library.ML --- a/src/Pure/library.ML Wed Dec 10 17:19:25 2008 +0100 +++ b/src/Pure/library.ML Thu Dec 11 17:55:51 2008 +0100 @@ -1,5 +1,4 @@ (* Title: Pure/library.ML - ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Author: Markus Wenzel, TU Muenchen @@ -491,7 +490,7 @@ | split_last [x] = ([], x) | split_last (x :: xs) = apfst (cons x) (split_last xs); -(*find the position of an element in a list*) +(*find position of first element satisfying a predicate*) fun find_index pred = let fun find (_: int) [] = ~1 | find n (x :: xs) = if pred x then n else find (n + 1) xs;