polished definition of find_index_eq

--- a/src/Pure/library.ML	Mon Nov 10 15:05:41 1997 +0100
+++ b/src/Pure/library.ML	Mon Nov 10 15:06:58 1997 +0100
@@ -249,7 +249,7 @@
   let fun find _ []      = ~1
         | find n (x::xs) = if pred x then n else find (n+1) xs
   in find 0 end;
-fun find_index_eq x = find_index (fn y => y = x);
+fun find_index_eq x = find_index (equal x);
 
 (*flatten a list of lists to a list*)
 fun flat (ls: 'c list list) : 'c list = foldr (op @) (ls, []);