src/Pure/proofterm.ML
changeset 12293 ce14a4faeded
parent 12279 dc3020e938e2
child 12294 2ef49890aede
     1.1 --- a/src/Pure/proofterm.ML	Sat Nov 24 17:01:00 2001 +0100
     1.2 +++ b/src/Pure/proofterm.ML	Sat Nov 24 17:02:39 2001 +0100
     1.3 @@ -1053,8 +1053,7 @@
     1.4    val finish = I;
     1.5    val prep_ext = I;
     1.6    fun merge ((rules1, procs1), (rules2, procs2)) =
     1.7 -    (merge_lists rules1 rules2,
     1.8 -     generic_merge (uncurry equal o pairself fst) I I procs1 procs2);
     1.9 +    (merge_lists rules1 rules2, merge_alists procs1 procs2);
    1.10    fun print _ _ = ();
    1.11  end;
    1.12