--- a/src/Pure/sorts.ML Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/sorts.ML Mon Feb 06 20:58:57 2006 +0100
@@ -180,7 +180,7 @@
fun mg_domain (classes, arities) a S =
let
fun dom c =
- (case AList.lookup (op =) (Symtab.lookup_multi arities a) c of
+ (case AList.lookup (op =) (Symtab.lookup_list 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);
@@ -241,7 +241,7 @@
else
let val ((solved', failed'), ws) = witn_sorts (S :: path) (solved_failed, SS) in
if forall is_some ws then
- let val w = (Type (t, map (#1 o valOf) ws), S)
+ let val w = (Type (t, map (#1 o the) ws), S)
in ((w :: solved', failed'), SOME w) end
else witn_types path ts ((solved', failed'), S)
end