# HG changeset patch
# User wenzelm
# Date 1120672833 -7200
# Node ID 1c8317722b4c587cccc6cd7be90013f7cbaeb389
# Parent  9a9c034f1d574eef7ec684f034928abb9cb4d0db
tuned eq_ix;

diff -r 9a9c034f1d57 -r 1c8317722b4c src/Pure/term.ML
--- 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