# HG changeset patch
# User wenzelm
# Date 1139255937 -3600
# Node ID 427df66052a1b510b4094e06e023e57546ef1d1d
# Parent  29d39c10822e6929927f2cb24562eb948de6ec17
TableFun: renamed xxx_multi to xxx_list;

diff -r 29d39c10822e -r 427df66052a1 src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Mon Feb 06 20:58:56 2006 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Mon Feb 06 20:58:57 2006 +0100
@@ -26,7 +26,7 @@
   val empty = Symtab.empty;
   val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge_multi' (Drule.eq_thm_prop o pairself fst);
+  fun merge _ = Symtab.merge_list (Drule.eq_thm_prop o pairself fst);
   fun print _ _ = ();
 end);
 
@@ -44,7 +44,7 @@
     val (s, _) = const_of (prop_of thm);
   in
     if Pattern.pattern (lhs_of thm) then
-      CodegenData.put (Symtab.update_multi (s, (thm, optmod)) tab) thy
+      CodegenData.put (Symtab.update_list (s, (thm, optmod)) tab) thy
     else (warn thm; thy)
   end handle TERM _ => (warn thm; thy)));
 
diff -r 29d39c10822e -r 427df66052a1 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Feb 06 20:58:56 2006 +0100
+++ b/src/HOL/Tools/record_package.ML	Mon Feb 06 20:58:57 2006 +0100
@@ -413,7 +413,7 @@
     fun varify (a, S) = TVar ((a, midx), S);
     val varifyT = map_type_tfree varify;
     val {records,extfields,...} = RecordsData.get thy;
-    val (flds,(more,_)) = split_last (Symtab.lookup_multi extfields name);
+    val (flds,(more,_)) = split_last (Symtab.lookup_list extfields name);
     val args = map varifyT (snd (#extension (the (Symtab.lookup records recname))));
 
     val (subst,_) = fold (Sign.typ_unify thy) (but_last args ~~ but_last Ts) (Vartab.empty,0);
@@ -839,7 +839,7 @@
 local
 fun eq (s1:string) (s2:string) = (s1 = s2);
 fun has_field extfields f T =
-     exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_multi extfields eN))
+     exists (fn (eN,_) => exists (eq f o fst) (Symtab.lookup_list extfields eN))
        (dest_recTs T);
 in
 (* record_simproc *)
diff -r 29d39c10822e -r 427df66052a1 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/Syntax/syntax.ML	Mon Feb 06 20:58:57 2006 +0100
@@ -101,10 +101,10 @@
 
 (* print (ast) translations *)
 
-fun lookup_tr' tab c = map fst (Symtab.lookup_multi tab c);
-fun extend_tr'tab trfuns = fold_rev Symtab.update_multi trfuns;
-fun remove_tr'tab trfuns = fold (Symtab.remove_multi SynExt.eq_trfun) trfuns;
-fun merge_tr'tabs tab1 tab2 = Symtab.merge_multi' SynExt.eq_trfun (tab1, tab2);
+fun lookup_tr' tab c = map fst (Symtab.lookup_list tab c);
+fun extend_tr'tab trfuns = fold_rev Symtab.update_list trfuns;
+fun remove_tr'tab trfuns = fold (Symtab.remove_list SynExt.eq_trfun) trfuns;
+fun merge_tr'tabs tab1 tab2 = Symtab.merge_list SynExt.eq_trfun (tab1, tab2);
 
 
 
@@ -154,9 +154,9 @@
 
 (* empty, extend, merge ruletabs *)
 
-val extend_ruletab = fold_rev (fn r => Symtab.update_multi (Ast.head_of_rule r, r));
-val remove_ruletab = fold (fn r => Symtab.remove_multi (op =) (Ast.head_of_rule r, r));
-fun merge_ruletabs tab1 tab2 = Symtab.merge_multi' (op =) (tab1, tab2);
+val extend_ruletab = fold_rev (fn r => Symtab.update_list (Ast.head_of_rule r, r));
+val remove_ruletab = fold (fn r => Symtab.remove_list (op =) (Ast.head_of_rule r, r));
+fun merge_ruletabs tab1 tab2 = Symtab.merge_list (op =) (tab1, tab2);
 
 
 
@@ -403,7 +403,7 @@
     val asts = read_asts context is_logtype syn false (SynExt.typ_to_nonterm ty) str;
   in
     SynTrans.asts_to_terms context (lookup_tr parse_trtab)
-      (map (Ast.normalize_ast (Symtab.lookup_multi parse_ruletab)) asts)
+      (map (Ast.normalize_ast (Symtab.lookup_list parse_ruletab)) asts)
   end;
 
 
@@ -487,7 +487,7 @@
   in
     prt_t context curried prtabs (lookup_tr' print_ast_trtab)
       (lookup_tokentr tokentrtab (! print_mode))
-      (Ast.normalize_ast (Symtab.lookup_multi print_ruletab) ast)
+      (Ast.normalize_ast (Symtab.lookup_list print_ruletab) ast)
   end;
 
 val pretty_term = pretty_t Printer.term_to_ast Printer.pretty_term_ast;
diff -r 29d39c10822e -r 427df66052a1 src/Pure/Thy/thm_database.ML
--- a/src/Pure/Thy/thm_database.ML	Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/Thy/thm_database.ML	Mon Feb 06 20:58:57 2006 +0100
@@ -105,7 +105,7 @@
       "val " ^ bname ^ " = thm" ^ (if singleton then "" else "s") ^ " " ^ quote xname;
   in
     Symtab.keys thms |> List.mapPartial prune
-    |> Symtab.make_multi |> Symtab.dest |> sort_wrt #1
+    |> Symtab.make_list |> Symtab.dest |> sort_wrt #1
     |> map (fn (prfx, entries) =>
       entries |> sort_wrt #1 |> map mk_thm |> cat_lines |> mk_struct prfx)
     |> cat_lines
diff -r 29d39c10822e -r 427df66052a1 src/Pure/context.ML
--- a/src/Pure/context.ML	Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/context.ML	Mon Feb 06 20:58:57 2006 +0100
@@ -416,7 +416,7 @@
 
 fun dest_data name_of tab =
   map name_of (Inttab.keys tab)
-  |> map (rpair ()) |> Symtab.make_multi |> Symtab.dest
+  |> map (rpair ()) |> Symtab.make_list |> Symtab.dest
   |> map (apsnd length)
   |> map (fn (name, 1) => name | (name, n) => name ^ enclose "[" "]" (string_of_int n));
 
diff -r 29d39c10822e -r 427df66052a1 src/Pure/fact_index.ML
--- a/src/Pure/fact_index.ML	Mon Feb 06 20:58:56 2006 +0100
+++ b/src/Pure/fact_index.ML	Mon Feb 06 20:58:57 2006 +0100
@@ -64,8 +64,8 @@
     val (cs, xs) = fold (index_thm known) ths ([], []);
 
     val facts' = fact :: facts;
-    val consts' = consts |> fold (fn c => Symtab.update_multi (c, entry)) cs;
-    val frees' = frees |> fold (fn x => Symtab.update_multi (x, entry)) xs;
+    val consts' = consts |> fold (fn c => Symtab.update_list (c, entry)) cs;
+    val frees' = frees |> fold (fn x => Symtab.update_list (x, entry)) xs;
     val props' = props |> K do_props ?
       fold (fn th => Net.insert_term (K false) (Thm.prop_of th, th)) ths;
   in Index {facts = facts', consts = consts', frees = frees', props = props'} end;
@@ -89,8 +89,8 @@
 
 fun find idx ([], []) = facts idx
   | find (Index {consts, frees, ...}) (cs, xs) =
-      (map (Symtab.lookup_multi consts) cs @
-        map (Symtab.lookup_multi frees) xs) |> intersects |> map #2;
+      (map (Symtab.lookup_list consts) cs @
+        map (Symtab.lookup_list frees) xs) |> intersects |> map #2;
 
 end
 
diff -r 29d39c10822e -r 427df66052a1 src/Pure/sorts.ML
--- 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