diff -r a788a05fb81b -r 3d80209e9a53 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Mon Aug 29 16:18:03 2005 +0200
+++ b/src/Pure/sorts.ML	Mon Aug 29 16:18:04 2005 +0200
@@ -180,7 +180,7 @@
 fun mg_domain (classes, arities) a S =
   let
     fun dom c =
-      (case Library.assoc_string (Symtab.lookup_multi (arities, a), c) of
+      (case AList.lookup (op =) (Symtab.lookup_multi (arities, a)) c of
         NONE => raise DOMAIN (a, c)
       | SOME Ss => Ss);
     fun dom_inter c Ss = ListPair.map (inter_sort classes) (dom c, Ss);