# HG changeset patch
# User wenzelm
# Date 861207405 -7200
# Node ID 071bfb16586fbb21449597935f8d541b2fc3a8cc
# Parent  7837471d2f27a95760118638801509cb09bbf2bf
tuned type of eq_ix, mem_ix;

diff -r 7837471d2f27 -r 071bfb16586f src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Apr 16 18:16:02 1997 +0200
+++ b/src/Pure/term.ML	Wed Apr 16 18:16:45 1997 +0200
@@ -324,10 +324,10 @@
 (** Equality, membership and insertion of indexnames (string*ints) **)
 
 (*optimized equality test for indexnames.  Yields a huge gain under Poly/ML*)
-fun eq_ix ((a:string, i:int), (a',i')) = (a=a') andalso i=i';
+fun eq_ix ((a, i):indexname, (a',i'):indexname) = (a=a') andalso i=i';
 
 (*membership in a list, optimized version for indexnames*)
-fun mem_ix (x:string*int, []) = false
+fun mem_ix (_, []) = false
   | mem_ix (x, y :: ys) = eq_ix(x,y) orelse mem_ix (x, ys);
 
 (*insertion into list, optimized version for indexnames*)