polished definition of find_index_eq
authoroheimb
Mon Nov 10 15:06:58 1997 +0100 (1997-11-10)
changeset 41941c2553be1821
parent 4193 a8e252c91dba
child 4195 7f7bf0bd0f63
polished definition of find_index_eq
src/Pure/library.ML
     1.1 --- a/src/Pure/library.ML	Mon Nov 10 15:05:41 1997 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Nov 10 15:06:58 1997 +0100
     1.3 @@ -249,7 +249,7 @@
     1.4    let fun find _ []      = ~1
     1.5          | find n (x::xs) = if pred x then n else find (n+1) xs
     1.6    in find 0 end;
     1.7 -fun find_index_eq x = find_index (fn y => y = x);
     1.8 +fun find_index_eq x = find_index (equal x);
     1.9  
    1.10  (*flatten a list of lists to a list*)
    1.11  fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);