slight refinements

--- a/src/Pure/General/alist.ML	Wed Dec 21 15:18:36 2005 +0100
+++ b/src/Pure/General/alist.ML	Wed Dec 21 15:18:57 2005 +0100
@@ -26,7 +26,6 @@
   val merge: ('a * 'a -> bool) -> ('b * 'b -> bool)
     -> ('a * 'b) list * ('a * 'b) list -> ('a * 'b) list      (*exception DUP*)
   val find: ('a * 'b -> bool) -> ('c * 'b) list -> 'a -> 'c list
-  val string_of_alist: ('a -> string) -> ('b -> string) -> ('a * 'b) list -> string
 end;
 
 structure AList: ALIST =
@@ -108,9 +107,4 @@
         val values = find eq xs value';
       in if eq (value', value) then key :: values else values end;
 
-fun string_of_alist string_of_key string_of_value =
-  map (fn (key, value) => string_of_key key ^ " -> " ^ string_of_value value)
-  #> commas
-  #> enclose "[" "]"
-
 end;

--- a/src/Pure/General/name_mangler.ML	Wed Dec 21 15:18:36 2005 +0100
+++ b/src/Pure/General/name_mangler.ML	Wed Dec 21 15:18:57 2005 +0100
@@ -11,11 +11,17 @@
   type ctxt
   type src
   type T
-  exception DUP of src
-  val mk_unique: ('b * 'b -> bool) -> ('a * int -> 'b) -> 'a -> 'b list -> 'b * 'b list
+  val mk_unique: ('b * 'b -> bool) -> ('a * int -> 'b)
+    -> 'a -> 'b list -> 'b * 'b list
+  val mk_unique_multi: ('b * 'b -> bool) -> ('a * int -> 'b)
+    -> 'a list -> 'b list -> 'b list * 'b list
+  val empty: T
   val get: ctxt -> T -> src -> string
   val rev: ctxt -> T -> string -> src
   val declare: ctxt -> src -> T -> string * T
+  val declare_multi: ctxt -> src list -> T -> string list * T
+  val merge: T * T -> T
+  val dest: T -> (src * string) list
 end;
 
 functor NameManglerFun (
@@ -38,8 +44,6 @@
 type src = src;
 type T = string Srctab.table * src Symtab.table;
 
-exception DUP of src;
-
 fun mk_unique eq mk seed used =
   let
     fun mk_name i =
@@ -53,6 +57,21 @@
     val name = mk_name 0;
   in (name, name :: used) end;
 
+fun mk_unique_multi eq mk seeds used =
+  let
+    fun mk_names i =
+      let
+        val names = map (fn seed => mk (seed, i)) seeds
+      in
+        if null (gen_inter eq (used, names))
+        then names
+        else mk_names (i+1)
+      end;
+    val names = mk_names 0;
+  in (names, fold cons names used) end;
+
+val empty = (Srctab.empty, Symtab.empty);
+
 fun get ctxt (tab_f, _) x =
   case Srctab.lookup tab_f x
    of SOME s => s
@@ -80,4 +99,31 @@
         end
     | SOME s => (s, tabs)
 
+fun declare_multi ctxt xs (tabs as (tab_f, tab_r)) =
+  let
+    val xs' = map (maybe_unique ctxt) xs
+  in
+    if forall is_some xs'
+    then (map the xs', tabs)
+    else
+      let
+        fun mk_it (seed, i) =
+          let
+            val name = mk ctxt (seed, i)
+          in if is_valid ctxt name then name
+          else mk_it (seed, i+1) end;
+        val names = (fst oooo mk_unique_multi) (op =) mk_it xs [];
+      in
+        (names,
+         (tab_f |> fold2 (curry Srctab.update) xs names,
+          tab_r |> fold2 (curry Symtab.update) names xs))
+      end
+  end;
+
+fun merge ((tab_f_1, tab_r_1), (tab_f_2, tab_r_2)) =
+  (Srctab.merge (op = : string * string -> bool) (tab_f_1, tab_f_2),
+   Symtab.merge (eq_ord ord) (tab_r_1, tab_r_2));
+
+fun dest (tab_f, _) = Srctab.dest tab_f;
+
 end;
\ No newline at end of file