# HG changeset patch
# User wenzelm
# Date 1006617386 -3600
# Node ID 6490fc7b3eed0534176088c403017324241d14e0
# Parent  131e743d168ace2982ebf99b3381a041fdfebe17
gen_merge_lists;

diff -r 131e743d168a -r 6490fc7b3eed src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Sat Nov 24 16:55:56 2001 +0100
+++ b/src/Pure/meta_simplifier.ML	Sat Nov 24 16:56:26 2001 +0100
@@ -213,11 +213,11 @@
        bounds = bounds2, prems = prems2, ...}) =
       mk_mss
        (Net.merge (rules1, rules2, eq_rrule),
-        (generic_merge (eq_cong o pairself snd) I I congs1 congs2,
+        (gen_merge_lists (eq_cong o pairself snd) congs1 congs2,
         merge_lists weak1 weak2),
         Net.merge (procs1, procs2, eq_simproc),
         merge_lists bounds1 bounds2,
-        generic_merge eq_prem I I prems1 prems2,
+        gen_merge_lists eq_prem prems1 prems2,
         mk_rews, termless, depth);