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