# HG changeset patch
# User oheimb
# Date 879170818 -3600
# Node ID 1c2553be18218f2bd43df79ebe7267699c9c3bf7
# Parent  a8e252c91dba1bfe1fa9d98780385d573dbba6a9
polished definition of find_index_eq

diff -r a8e252c91dba -r 1c2553be1821 src/Pure/library.ML
--- 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, []);