src/Pure/type_infer.ML
changeset 16668 fdb4992cf1d2
parent 16366 6ff17d08c3d5
child 17271 2756a73f63a5
--- a/src/Pure/type_infer.ML	Fri Jul 01 22:35:20 2005 +0200
+++ b/src/Pure/type_infer.ML	Fri Jul 01 22:35:41 2005 +0200
@@ -448,7 +448,7 @@
 
 fun get_sort tsig def_sort map_sort raw_env =
   let
-    fun eq ((xi, S), (xi', S')) =
+    fun eq ((xi: indexname, S), (xi', S')) =
       xi = xi' andalso Type.eq_sort tsig (S, S');
 
     val env = gen_distinct eq (map (apsnd map_sort) raw_env);