# HG changeset patch
# User wenzelm
# Date 1139255936 -3600
# Node ID 29d39c10822e6929927f2cb24562eb948de6ec17
# Parent  d8143510868898a91879328c3e1f9b549ffdcdb6
replaced Symtab.merge_multi by local merge_rules;

diff -r d81435108688 -r 29d39c10822e src/HOL/Tools/inductive_codegen.ML
--- a/src/HOL/Tools/inductive_codegen.ML	Mon Feb 06 20:58:54 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Mon Feb 06 20:58:56 2006 +0100
@@ -18,6 +18,10 @@
 
 (**** theory data ****)
 
+fun merge_rules tabs =
+  Symtab.join (fn _ => fn (ths, ths') =>
+    SOME (gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths')) tabs;
+
 structure CodegenData = TheoryDataFun
 (struct
   val name = "HOL/inductive_codegen";
@@ -31,11 +35,9 @@
   val extend = I;
   fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
     {intros=intros2, graph=graph2, eqns=eqns2}) =
-    {intros = Symtab.merge_multi (Drule.eq_thm_prop o pairself fst)
-       (intros1, intros2),
+    {intros = merge_rules (intros1, intros2),
      graph = Graph.merge (K true) (graph1, graph2),
-     eqns = Symtab.merge_multi (Drule.eq_thm_prop o pairself fst)
-       (eqns1, eqns2)};
+     eqns = merge_rules (eqns1, eqns2)};
   fun print _ _ = ();
 end);
 
@@ -56,7 +58,7 @@
           let val cs = foldr add_term_consts [] (prems_of thm)
           in CodegenData.put
             {intros = intros |>
-             Symtab.update (s, Symtab.lookup_multi intros s @ [(thm, thyname_of s)]),
+             Symtab.update (s, Symtab.lookup_list intros s @ [(thm, thyname_of s)]),
              graph = foldr (uncurry (Graph.add_edge o pair s))
                (Library.foldl add_node (graph, s :: cs)) cs,
              eqns = eqns} thy
@@ -66,7 +68,7 @@
         Const (s, _) =>
           CodegenData.put {intros = intros, graph = graph,
              eqns = eqns |> Symtab.update
-               (s, Symtab.lookup_multi eqns s @ [(thm, thyname_of s)])} thy
+               (s, Symtab.lookup_list eqns s @ [(thm, thyname_of s)])} thy
       | _ => (warn thm; thy))
     | _ => (warn thm; thy))
   end));