changeset 12286 | fe218fdc961a |
parent 12123 | 739eba13e2cd |
child 12296 | 45269a593e1b |
--- a/src/Pure/sign.ML Sat Nov 24 16:56:26 2001 +0100 +++ b/src/Pure/sign.ML Sat Nov 24 16:57:34 2001 +0100 @@ -1086,7 +1086,7 @@ (* merge_stamps *) fun merge_stamps stamps1 stamps2 = - let val stamps = merge_rev_lists stamps1 stamps2 in + let val stamps = merge_lists' stamps2 stamps1 in (case duplicates (map ! stamps) of [] => stamps | dups => raise TERM ("Attempt to merge different versions of theories "