simplified TableFun.join;
authorwenzelm
Sun Feb 12 21:34:18 2006 +0100 (2006-02-12)
changeset 19025596fb1eb7856
parent 19024 80eb6640f3d5
child 19026 87cd1ecae3a4
simplified TableFun.join;
src/HOL/Tools/inductive_codegen.ML
src/Pure/Isar/locale.ML
src/Pure/Tools/codegen_package.ML
src/Pure/Tools/codegen_thingol.ML
src/Pure/defs.ML
     1.1 --- a/src/HOL/Tools/inductive_codegen.ML	Sun Feb 12 20:32:59 2006 +0100
     1.2 +++ b/src/HOL/Tools/inductive_codegen.ML	Sun Feb 12 21:34:18 2006 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4  
     1.5  fun merge_rules tabs =
     1.6    Symtab.join (fn _ => fn (ths, ths') =>
     1.7 -    SOME (gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths')) tabs;
     1.8 +    gen_merge_lists (Drule.eq_thm_prop o pairself fst) ths ths') tabs;
     1.9  
    1.10  structure CodegenData = TheoryDataFun
    1.11  (struct
     2.1 --- a/src/Pure/Isar/locale.ML	Sun Feb 12 20:32:59 2006 +0100
     2.2 +++ b/src/Pure/Isar/locale.ML	Sun Feb 12 21:34:18 2006 +0100
     2.3 @@ -193,7 +193,7 @@
     2.4  
     2.5    (* joining of registrations: prefix and attributes of left theory,
     2.6       thms are equal, no attempt to subsumption testing *)
     2.7 -  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => SOME reg) (r1, r2);
     2.8 +  fun join (r1, r2) = Termtab.join (fn _ => fn (reg, _) => reg) (r1, r2);
     2.9  
    2.10    fun dest regs = map (apfst untermify) (Termtab.dest regs);
    2.11  
    2.12 @@ -267,7 +267,6 @@
    2.13  
    2.14    fun join_locs _ ({predicate, import, elems, params, abbrevs, regs}: locale,
    2.15        {elems = elems', abbrevs = abbrevs', regs = regs', ...}: locale) =
    2.16 -    SOME
    2.17       {predicate = predicate,
    2.18        import = import,
    2.19        elems = gen_merge_lists (eq_snd (op =)) elems elems',
    2.20 @@ -276,7 +275,7 @@
    2.21        regs = merge_alists regs regs'};
    2.22    fun merge _ ((space1, locs1, regs1), (space2, locs2, regs2)) =
    2.23      (NameSpace.merge (space1, space2), Symtab.join join_locs (locs1, locs2),
    2.24 -     Symtab.join (K (SOME o Registrations.join)) (regs1, regs2));
    2.25 +     Symtab.join (K Registrations.join) (regs1, regs2));
    2.26  
    2.27    fun print _ (space, locs, _) =
    2.28      Pretty.strs ("locales:" :: map #1 (NameSpace.extern_table (space, locs)))
     3.1 --- a/src/Pure/Tools/codegen_package.ML	Sun Feb 12 20:32:59 2006 +0100
     3.2 +++ b/src/Pure/Tools/codegen_package.ML	Sun Feb 12 21:34:18 2006 +0100
     3.3 @@ -304,8 +304,7 @@
     3.4      modl = merge_module (modl1, modl2),
     3.5      gens = merge_gens (gens1, gens2),
     3.6      logic_data = merge_logic_data (logic_data1, logic_data2),
     3.7 -    target_data = Symtab.join (K (merge_target_data #> SOME))
     3.8 -      (target_data1, target_data2)
     3.9 +    target_data = Symtab.join (K merge_target_data) (target_data1, target_data2)
    3.10    };
    3.11    fun print _ _ = ();
    3.12  end);
     4.1 --- a/src/Pure/Tools/codegen_thingol.ML	Sun Feb 12 20:32:59 2006 +0100
     4.2 +++ b/src/Pure/Tools/codegen_thingol.ML	Sun Feb 12 21:34:18 2006 +0100
     4.3 @@ -704,13 +704,12 @@
     4.4  
     4.5  fun merge_module modl12 =
     4.6    let
     4.7 -    fun join_module (Module m1, Module m2) =
     4.8 -          (SOME o Module) (merge_module (m1, m2))
     4.9 -      | join_module (Def d1, Def d2) =
    4.10 -          if eq_def (d1, d2) then (SOME o Def) d1 else NONE
    4.11 -      | join_module _ =
    4.12 -          NONE
    4.13 -  in Graph.join (K join_module) modl12 end;
    4.14 +    fun join_module _ (Module m1, Module m2) =
    4.15 +          Module (merge_module (m1, m2))
    4.16 +      | join_module name (Def d1, Def d2) =
    4.17 +          if eq_def (d1, d2) then Def d1 else raise Graph.DUP name
    4.18 +      | join_module name _ = raise Graph.DUP name
    4.19 +  in Graph.join join_module modl12 end;
    4.20  
    4.21  fun partof names modl =
    4.22    let
     5.1 --- a/src/Pure/defs.ML	Sun Feb 12 20:32:59 2006 +0100
     5.2 +++ b/src/Pure/defs.ML	Sun Feb 12 21:34:18 2006 +0100
     5.3 @@ -76,8 +76,8 @@
     5.4      val consts' = (consts1, consts2) |> Graph.merge_acyclic (K true)
     5.5        handle Graph.CYCLES cycles => err_cyclic cycles;
     5.6      val specified' = (specified1, specified2) |> Symtab.join (fn c => fn (orig_specs1, specs2) =>
     5.7 -      SOME (Inttab.fold (fn spec2 => fn specs1 =>
     5.8 -        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1));
     5.9 +      Inttab.fold (fn spec2 => fn specs1 =>
    5.10 +        (check_specified c spec2 orig_specs1; Inttab.update spec2 specs1)) specs2 orig_specs1);
    5.11    in make_defs (consts', specified') end;
    5.12  
    5.13  end;