# HG changeset patch
# User wenzelm
# Date 932741455 -7200
# Node ID 601f930d373973a832761c757029aff5e12088df
# Parent  febce8eee48791665f99f388e3833649caec18bf
replace assoc lists by Symtab.table;

diff -r febce8eee487 -r 601f930d3739 src/Pure/display.ML
--- a/src/Pure/display.ML	Fri Jul 23 16:50:20 1999 +0200
+++ b/src/Pure/display.ML	Fri Jul 23 16:50:55 1999 +0200
@@ -176,7 +176,7 @@
       [Pretty.str "default:", Pretty.brk 1, prt_sort S];
 
     fun pretty_ty (t, n) = Pretty.block
-      [Pretty.str (Sign.cond_extern sg Sign.typeK t), Pretty.spc 1, Pretty.str (string_of_int n)];
+      [Pretty.str t, Pretty.spc 1, Pretty.str (string_of_int n)];
 
     fun pretty_abbr (t, (vs, rhs)) = Pretty.block
       [prt_typ (Type (t, map (fn v => TVar ((v, 0), [])) vs)),
@@ -189,8 +189,9 @@
 
     val {self = _, tsig, const_tab, syn = _, path, spaces, data} = Sign.rep_sg sg;
     val spaces' = Library.sort_wrt fst spaces;
-    val {classes, classrel, default, tycons, abbrs, arities} =
+    val {classes, classrel, default, tycons = type_tab, abbrs, arities} =
       Type.rep_tsig tsig;
+    val tycons = Sign.cond_extern_table sg Sign.typeK type_tab;
     val consts = Sign.cond_extern_table sg Sign.constK const_tab;
   in
     Pretty.writeln (Pretty.strs ("stamps:" :: Sign.stamp_names_of sg));
@@ -198,11 +199,11 @@
     Pretty.writeln (Pretty.strs ["name prefix:", NameSpace.pack path]);
     Pretty.writeln (Pretty.big_list "name spaces:" (map pretty_name_space spaces'));
     Pretty.writeln (pretty_classes classes);
-    Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel classrel));
+    Pretty.writeln (Pretty.big_list "class relation:" (map pretty_classrel (Symtab.dest classrel)));
     Pretty.writeln (pretty_default default);
     Pretty.writeln (Pretty.big_list "type constructors:" (map pretty_ty tycons));
-    Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr abbrs));
-    Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities arities)));
+    Pretty.writeln (Pretty.big_list "type abbreviations:" (map pretty_abbr (Symtab.dest abbrs)));
+    Pretty.writeln (Pretty.big_list "type arities:" (flat (map pretty_arities (Symtab.dest arities))));
     Pretty.writeln (Pretty.big_list "consts:" (map pretty_const consts))
   end;
 
diff -r febce8eee487 -r 601f930d3739 src/Pure/sorts.ML
--- a/src/Pure/sorts.ML	Fri Jul 23 16:50:20 1999 +0200
+++ b/src/Pure/sorts.ML	Fri Jul 23 16:50:55 1999 +0200
@@ -50,17 +50,17 @@
 
 (*
   classrel:
-    association list representing the proper subclass relation;
-    pairs (c, cs) represent the superclasses cs of c;
+    table representing the proper subclass relation; entries (c, cs)
+    represent the superclasses cs of c;
 
   arities:
-    two-fold association list of all type arities; (t, ars) means
+    table of association lists of all type arities; (t, ars) means
     that type constructor t has the arities ars; an element (c, Ss) of
-    ars represents the arity t::(Ss)c.
+    ars represents the arity t::(Ss)c;
 *)
 
-type classrel = (class * class list) list;
-type arities = (string * (class * sort list) list) list;
+type classrel = (class list) Symtab.table;
+type arities = ((class * sort list) list) Symtab.table;
 
 
 (* print sorts and arities *)
@@ -82,7 +82,7 @@
 fun class_eq _ (c1, c2:class) = c1 = c2;
 
 fun class_less classrel (c1, c2) =
-  (case assoc (classrel, c1) of
+  (case Symtab.lookup (classrel, c1) of
      Some cs => c2 mem_string cs
    | None => false);
 
@@ -137,9 +137,11 @@
 (* mg_domain *)                 (*exception TYPE*)
 
 fun mg_dom arities a c =
-  (case assoc2 (arities, (a, c)) of
-    None => raise TYPE ("No way to get " ^ a ^ "::" ^ c ^ ".", [], [])
-  | Some Ss => Ss);
+  let fun err () = raise TYPE ("No way to get " ^ a ^ "::" ^ c ^ ".", [], []) in
+    (case Symtab.lookup (arities, a) of
+      None => err ()
+    | Some ars => (case assoc (ars, c) of None => err () | Some Ss => Ss))
+  end;
 
 fun mg_domain _ _ _ [] = sys_error "mg_domain"  (*don't know number of args!*)
   | mg_domain classrel arities a S =
@@ -168,7 +170,7 @@
 (* FIXME improve: proper sorts; non-base, non-ground types (vars from hyps) *)
 fun nonempty_sort classrel _ _ [] = true
   | nonempty_sort classrel arities hyps S =
-      exists (exists (fn (c, Ss) => [c] = S andalso null Ss) o snd) arities
+      Symtab.exists (exists (fn (c, Ss) => [c] = S andalso null Ss) o snd) arities
         orelse exists (fn S' => sort_le classrel (S', S)) hyps;
 
 end;