merge_ss: plain merge of prems;

--- a/src/Pure/meta_simplifier.ML	Sun Jun 03 23:16:48 2007 +0200
+++ b/src/Pure/meta_simplifier.ML	Sun Jun 03 23:16:49 2007 +0200
@@ -801,7 +801,7 @@
       loop_tacs = loop_tacs2, solvers = (unsafe_solvers2, solvers2)}) = ss2;
 
     val rules' = Net.merge eq_rrule (rules1, rules2);
-    val prems' = gen_merge_lists Thm.eq_thm_prop prems1 prems2;
+    val prems' = merge Thm.eq_thm_prop (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 (eq_cong o pairself #2) (congs1, congs2);