src/Pure/library.ML
changeset 4188 1025a27b08f9
parent 4181 fcc8b47e4c49
child 4194 1c2553be1821
     1.1 --- a/src/Pure/library.ML	Fri Nov 07 17:51:26 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Fri Nov 07 18:02:15 1997 +0100
     1.3 @@ -245,10 +245,11 @@
     1.4  
     1.5  
     1.6  (*find the position of an element in a list*)
     1.7 -fun find (x, ys) =
     1.8 -  let fun f (y :: ys, i) = if x = y then i else f (ys, i + 1)
     1.9 -        | f (_, _) = raise LIST "find"
    1.10 -  in f (ys, 0) end;
    1.11 +fun find_index (pred: 'a->bool) : 'a list -> int =
    1.12 +  let fun find _ []      = ~1
    1.13 +        | find n (x::xs) = if pred x then n else find (n+1) xs
    1.14 +  in find 0 end;
    1.15 +fun find_index_eq x = find_index (fn y => y = x);
    1.16  
    1.17  (*flatten a list of lists to a list*)
    1.18  fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);
    1.19 @@ -294,10 +295,10 @@
    1.20        | Some y => y :: mapfilter f xs);
    1.21  
    1.22  
    1.23 -fun find_first _ [] = None
    1.24 -  | find_first pred (x :: xs) =
    1.25 -      if pred x then Some x else find_first pred xs;
    1.26 -
    1.27 +fun find_first pred = let
    1.28 +  fun f [] = None
    1.29 +  |   f (x :: xs) = if pred x then Some x else f  xs
    1.30 +  in f end;
    1.31  
    1.32  (* lists of pairs *)
    1.33