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);