gen_merge_lists;
authorwenzelm
Sat, 24 Nov 2001 16:56:26 +0100
changeset 12285 6490fc7b3eed
parent 12284 131e743d168a
child 12286 fe218fdc961a
gen_merge_lists;
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);