gen_merge_lists;
authorwenzelm
Sat Nov 24 16:56:26 2001 +0100 (2001-11-24)
changeset 122856490fc7b3eed
parent 12284 131e743d168a
child 12286 fe218fdc961a
gen_merge_lists;
src/Pure/meta_simplifier.ML
     1.1 --- a/src/Pure/meta_simplifier.ML	Sat Nov 24 16:55:56 2001 +0100
     1.2 +++ b/src/Pure/meta_simplifier.ML	Sat Nov 24 16:56:26 2001 +0100
     1.3 @@ -213,11 +213,11 @@
     1.4         bounds = bounds2, prems = prems2, ...}) =
     1.5        mk_mss
     1.6         (Net.merge (rules1, rules2, eq_rrule),
     1.7 -        (generic_merge (eq_cong o pairself snd) I I congs1 congs2,
     1.8 +        (gen_merge_lists (eq_cong o pairself snd) congs1 congs2,
     1.9          merge_lists weak1 weak2),
    1.10          Net.merge (procs1, procs2, eq_simproc),
    1.11          merge_lists bounds1 bounds2,
    1.12 -        generic_merge eq_prem I I prems1 prems2,
    1.13 +        gen_merge_lists eq_prem prems1 prems2,
    1.14          mk_rews, termless, depth);
    1.15  
    1.16