# HG changeset patch
# User wenzelm
# Date 1139255997 -3600
# Node ID 8c3abd63bce3ac2e9e3d6240a500aab588638a1c
# Parent  c050ae1f8f52545867f67125ff1d780b9a6a3e8f
TableFun: renamed xxx_multi to xxx_list;
tuned;

diff -r c050ae1f8f52 -r 8c3abd63bce3 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Feb 06 20:59:56 2006 +0100
+++ b/src/Pure/Syntax/printer.ML	Mon Feb 06 20:59:57 2006 +0100
@@ -191,7 +191,7 @@
 
 type prtabs = (string * ((symb list * int * int) list) Symtab.table) list;
 
-fun mode_tab prtabs mode = if_none (AList.lookup (op =) prtabs mode) Symtab.empty;
+fun mode_tab prtabs mode = the_default Symtab.empty (AList.lookup (op =) prtabs mode);
 fun mode_tabs prtabs modes = List.mapPartial (AList.lookup (op =) prtabs) (modes @ [""]);
 
 
@@ -248,13 +248,13 @@
     val tab = fold f fmts (mode_tab prtabs mode);
   in AList.update (op =) (mode, tab) prtabs end;
 
-fun extend_prtabs m = change_prtabs Symtab.update_multi m;
-fun remove_prtabs m = change_prtabs (Symtab.remove_multi (op =)) m;
+fun extend_prtabs m = change_prtabs Symtab.update_list m;
+fun remove_prtabs m = change_prtabs (Symtab.remove_list (op =)) m;
 
 fun merge_prtabs prtabs1 prtabs2 =
   let
     val modes = distinct (map fst (prtabs1 @ prtabs2));
-    fun merge m = (m, Symtab.merge_multi' (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
+    fun merge m = (m, Symtab.merge_list (op =) (mode_tab prtabs1 m, mode_tab prtabs2 m));
   in map merge modes end;
 
 
@@ -330,7 +330,7 @@
 
         (*find matching table entry, or print as prefix / postfix*)
         fun prnt ([], []) = prefixT tup
-          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_multi tb a, tbs)
+          | prnt ([], tb :: tbs) = prnt (Symtab.lookup_list tb a, tbs)
           | prnt ((pr, n, p') :: prnps, tbs) =
               if nargs = n then parT (pr, args, p, p')
               else if nargs > n andalso not type_mode then
diff -r c050ae1f8f52 -r 8c3abd63bce3 src/Pure/type.ML
--- a/src/Pure/type.ML	Mon Feb 06 20:59:56 2006 +0100
+++ b/src/Pure/type.ML	Mon Feb 06 20:59:57 2006 +0100
@@ -151,7 +151,7 @@
 local
 
 fun inst_typ env (Type (c, Ts)) = Type (c, map (inst_typ env) Ts)
-  | inst_typ env (T as TFree (x, _)) = if_none (AList.lookup (op =) env x) T
+  | inst_typ env (T as TFree (x, _)) = the_default T (AList.lookup (op =) env x)
   | inst_typ _ T = T;
 
 fun certify_typ normalize syntax tsig ty =
@@ -487,7 +487,7 @@
 
 fun insert_arities pp classes (t, ars) arities =
   let val ars' =
-    Symtab.lookup_multi arities t
+    Symtab.lookup_list arities t
     |> fold_rev (fold_rev (insert pp classes t)) (map (complete classes) ars)
   in Symtab.update (t, ars') arities end;