author | wenzelm |
Sat, 24 Nov 2001 17:02:39 +0100 | |
changeset 12293 | ce14a4faeded |
parent 12292 | c4090cc2aa15 |
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;