src/Pure/term.ML
changeset 16724 1c8317722b4c
parent 16710 3d6335ff3982
child 16787 b6b6e2faaa41
     1.1 --- a/src/Pure/term.ML	Wed Jul 06 20:00:31 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jul 06 20:00:33 2005 +0200
     1.3 @@ -766,7 +766,7 @@
     1.4  (** Equality, membership and insertion of indexnames (string*ints) **)
     1.5  
     1.6  (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
     1.7 -fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i';
     1.8 +fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
     1.9  
    1.10  (*membership in a list, optimized version for indexnames*)
    1.11  fun mem_ix (_, []) = false