tuned eq_ix;

--- a/src/Pure/term.ML	Wed Jul 06 20:00:31 2005 +0200
+++ b/src/Pure/term.ML	Wed Jul 06 20:00:33 2005 +0200
@@ -766,7 +766,7 @@
 (** Equality, membership and insertion of indexnames (string*ints) **)
 
 (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
-fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i';
+fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
 
 (*membership in a list, optimized version for indexnames*)
 fun mem_ix (_, []) = false