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