# HG changeset patch # User wenzelm # Date 1006617759 -3600 # Node ID ce14a4faededef7cf0020950bb0794e1697e5006 # Parent c4090cc2aa15ceb3cd986314376a170d169b96b7 use merge_lists, merge_alists; diff -r c4090cc2aa15 -r ce14a4faeded src/Pure/proofterm.ML --- 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;