tuned;

--- a/src/HOL/Algebra/ringsimp.ML	Sun Nov 08 16:30:41 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Sun Nov 08 18:42:57 2009 +0100
@@ -26,7 +26,7 @@
        identifier and operations identify the structure uniquely. *)
   val empty = [];
   val extend = I;
-  val merge = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
+  val merge = AList.join struct_eq (K Thm.merge_thms);
 );
 
 fun print_structures ctxt =

--- a/src/HOL/Tools/lin_arith.ML	Sun Nov 08 16:30:41 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Nov 08 18:42:57 2009 +0100
@@ -82,7 +82,7 @@
   fun merge
    ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
     {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
-   {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
+   {splits = Thm.merge_thms (splits1, splits2),
     inj_consts = Library.merge (op =) (inj_consts1, inj_consts2),
     discrete = Library.merge (op =) (discrete1, discrete2)};
 );

--- a/src/Pure/meta_simplifier.ML	Sun Nov 08 16:30:41 2009 +0100
+++ b/src/Pure/meta_simplifier.ML	Sun Nov 08 18:42:57 2009 +0100
@@ -772,7 +772,7 @@
         loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
 
       val rules' = Net.merge eq_rrule (rules1, rules2);
-      val prems' = merge Thm.eq_thm_prop (prems1, prems2);
+      val prems' = Thm.merge_thms (prems1, prems2);
       val bounds' = if #1 bounds1 < #1 bounds2 then bounds2 else bounds1;
       val depth' = if #1 depth1 < #1 depth2 then depth2 else depth1;
       val congs' = merge (Thm.eq_thm_prop o pairself #2) (congs1, congs2);