author | oheimb |
Mon Nov 10 15:06:58 1997 +0100 (1997-11-10) | |
changeset 4194 | 1c2553be1821 |
parent 4193 | a8e252c91dba |
child 4195 | 7f7bf0bd0f63 |
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, []);