canonical merge operations

--- a/src/HOL/Algebra/ringsimp.ML	Wed Apr 11 08:28:14 2007 +0200
+++ b/src/HOL/Algebra/ringsimp.ML	Wed Apr 11 08:28:15 2007 +0200
@@ -29,8 +29,7 @@
        identifier and operations identify the structure uniquely. *)
   val empty = [];
   val extend = I;
-  fun merge _ (structs1, structs2) = gen_merge_lists
-    (fn ((s1, _), (s2, _)) => struct_eq (s1, s2)) structs1 structs2;
+  fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
   fun print generic structs =
     let
       val ctxt = Context.proof_of generic;
@@ -64,14 +63,11 @@
 (** Attribute **)
 
 fun add_struct_thm s =
-  Thm.declaration_attribute (fn thm => fn ctxt =>
-    AlgebraData.map (fn structs =>
-      if AList.defined struct_eq structs s
-      then AList.map_entry struct_eq s (fn thms => thm :: thms) structs
-      else (s, [thm])::structs) ctxt);
+  Thm.declaration_attribute
+    (fn thm => AlgebraData.map (AList.map_default struct_eq (s, []) (insert Thm.eq_thm_prop thm)));
 fun del_struct s =
-  Thm.declaration_attribute (fn _ => fn ctxt =>
-    AlgebraData.map (AList.delete struct_eq s) ctxt);
+  Thm.declaration_attribute
+    (fn _ => AlgebraData.map (AList.delete struct_eq s));
 
 val attribute = Attrib.syntax
      (Scan.lift ((Args.add >> K true || Args.del >> K false) --| Args.colon ||

--- a/src/HOL/Tools/record_package.ML	Wed Apr 11 08:28:14 2007 +0200
+++ b/src/HOL/Tools/record_package.ML	Wed Apr 11 08:28:15 2007 +0200
@@ -299,9 +299,9 @@
       {selectors = Symtab.merge (K true) (sels1, sels2),
         updates = Symtab.merge (K true) (upds1, upds2),
         simpset = Simplifier.merge_ss (ss1, ss2)}
-      (Symtab.merge Thm.eq_thm (equalities1, equalities2))
-      (gen_merge_lists Thm.eq_thm extinjects1 extinjects2)
-      (Symtab.merge Thm.eq_thm (extsplit1,extsplit2))
+      (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
+      (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
+      (Symtab.merge Thm.eq_thm_prop (extsplit1,extsplit2))
       (Symtab.merge (fn ((a,b,c,d),(w,x,y,z))
                      => Thm.eq_thm (a,w) andalso Thm.eq_thm (b,x) andalso
                         Thm.eq_thm (c,y) andalso Thm.eq_thm (d,z))
@@ -384,11 +384,11 @@
   let
     val {records, sel_upd, equalities, extinjects, extsplit, splits, extfields,fieldext} =
           RecordsData.get thy;
-    val data = make_record_data records sel_upd equalities (extinjects@[thm]) extsplit
+    val data = make_record_data records sel_upd equalities (insert Thm.eq_thm_prop thm extinjects) extsplit
                  splits extfields fieldext;
   in RecordsData.put data thy end;
 
-fun get_extinjects thy = #extinjects (RecordsData.get thy);
+val get_extinjects = rev o #extinjects o RecordsData.get;
 
 (* access 'extsplit' *)
 

--- a/src/HOL/arith_data.ML	Wed Apr 11 08:28:14 2007 +0200
+++ b/src/HOL/arith_data.ML	Wed Apr 11 08:28:15 2007 +0200
@@ -209,8 +209,6 @@
 
 fun eq_arith_tactic (ArithTactic {id = id1, ...}, ArithTactic {id = id2, ...}) = (id1 = id2);
 
-val merge_arith_tactics = gen_merge_lists eq_arith_tactic;
-
 structure ArithTheoryData = TheoryDataFun
 (struct
   val name = "HOL/arith";
@@ -223,25 +221,25 @@
   val extend = I;
   fun merge _ ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1, tactics= tactics1},
              {splits= splits2, inj_consts= inj_consts2, discrete= discrete2, tactics= tactics2}) =
-   {splits = Drule.merge_rules (splits1, splits2),
-    inj_consts = merge_lists inj_consts1 inj_consts2,
-    discrete = merge_lists discrete1 discrete2,
-    tactics = merge_arith_tactics tactics1 tactics2};
+   {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
+    inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
+    discrete = Library.merge (op =) (discrete1, discrete2),
+    tactics = Library.merge eq_arith_tactic (tactics1, tactics2)};
   fun print _ _ = ();
 end);
 
 val arith_split_add = Thm.declaration_attribute (fn thm =>
   Context.mapping (ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
-    {splits= thm::splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})) I);
+    {splits= insert Thm.eq_thm_prop thm splits, inj_consts= inj_consts, discrete= discrete, tactics= tactics})) I);
 
 fun arith_discrete d = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
-  {splits = splits, inj_consts = inj_consts, discrete = d :: discrete, tactics= tactics});
+  {splits = splits, inj_consts = inj_consts, discrete = insert (op =) d discrete, tactics= tactics});
 
 fun arith_inj_const c = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
-  {splits = splits, inj_consts = c :: inj_consts, discrete = discrete, tactics= tactics});
+  {splits = splits, inj_consts = insert (op =) c inj_consts, discrete = discrete, tactics= tactics});
 
 fun arith_tactic_add tac = ArithTheoryData.map (fn {splits,inj_consts,discrete,tactics} =>
-  {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= merge_arith_tactics tactics [tac]});
+  {splits= splits, inj_consts= inj_consts, discrete= discrete, tactics= insert eq_arith_tactic tac tactics});
 
 
 signature HOL_LIN_ARITH_DATA =