simplified TableFun.join;

--- a/src/HOL/Tools/inductive_codegen.ML	Sun Feb 12 20:32:59 2006 +0100
+++ b/src/HOL/Tools/inductive_codegen.ML	Sun Feb 12 21:34:18 2006 +0100
@@ -20,7 +20,7 @@
 
 fun merge_rules tabs =
   Symtab.join (fn _ => fn (ths, ths') =>
-    SOME (gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths')) tabs;
+    gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths') tabs;
 
 structure CodegenData = TheoryDataFun
 (struct

--- a/src/Pure/Isar/locale.ML	Sun Feb 12 20:32:59 2006 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Feb 12 21:34:18 2006 +0100
@@ -193,7 +193,7 @@
 
   (* joining of registrations: prefix and attributes of left theory,
      thms are equal, no attempt to subsumption testing *)
-  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2);
+  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2);
 
   fun dest regs = map (apfst untermify) (Termtab.dest regs);
 
@@ -267,7 +267,6 @@
 
   fun join_locs _ ({predicate, import, elems, params, abbrevs, regs}: locale,
       {elems = elems', abbrevs = abbrevs', regs = regs', ...}: locale) =
-    SOME
      {predicate = predicate,
       import = import,
       elems = gen_merge_lists (eq_snd (op =)) elems elems',
@@ -276,7 +275,7 @@
       regs = merge_alists regs regs'};
   fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
     (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
-     Symtab.join (K (SOME o Registrations.join)) (regs1, regs2));
+     Symtab.join (K Registrations.join) (regs1, regs2));
 
   fun print _ (space, locs, _) =
     Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))

--- a/src/Pure/Tools/codegen_package.ML	Sun Feb 12 20:32:59 2006 +0100
+++ b/src/Pure/Tools/codegen_package.ML	Sun Feb 12 21:34:18 2006 +0100
@@ -304,8 +304,7 @@
     modl = merge_module (modl1, modl2),
     gens = merge_gens (gens1, gens2),
     logic_data = merge_logic_data (logic_data1, logic_data2),
-    target_data = Symtab.join (K (merge_target_data #> SOME))
-      (target_data1, target_data2)
+    target_data = Symtab.join (K merge_target_data) (target_data1, target_data2)
   };
   fun print _ _ = ();
 end);

--- a/src/Pure/Tools/codegen_thingol.ML	Sun Feb 12 20:32:59 2006 +0100
+++ b/src/Pure/Tools/codegen_thingol.ML	Sun Feb 12 21:34:18 2006 +0100
@@ -704,13 +704,12 @@
 
 fun merge_module modl12 =
   let
-    fun join_module (Module m1, Module m2) =
-          (SOME o Module) (merge_module (m1, m2))
-      | join_module (Def d1, Def d2) =
-          if eq_def (d1, d2) then (SOME o Def) d1 else NONE
-      | join_module _ =
-          NONE
-  in Graph.join (K join_module) modl12 end;
+    fun join_module _ (Module m1, Module m2) =
+          Module (merge_module (m1, m2))
+      | join_module name (Def d1, Def d2) =
+          if eq_def (d1, d2) then Def d1 else raise Graph.DUP name
+      | join_module name _ = raise Graph.DUP name
+  in Graph.join join_module modl12 end;
 
 fun partof names modl =
   let

--- a/src/Pure/defs.ML	Sun Feb 12 20:32:59 2006 +0100
+++ b/src/Pure/defs.ML	Sun Feb 12 21:34:18 2006 +0100
@@ -76,8 +76,8 @@
     val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
       handle Graph.CYCLES cycles => err_cyclic cycles;
     val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
-      SOME (Inttab.fold (fn spec2 => fn specs1 =>
-        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
+      Inttab.fold (fn spec2 => fn specs1 =>
+        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);
   in make_defs (consts', specified') end;
 
 end;