# HG changeset patch
# User wenzelm
# Date 1006617454 -3600
# Node ID fe218fdc961a35c5b4a6a4fe0e22fdacfb0f4849
# Parent  6490fc7b3eed0534176088c403017324241d14e0
merge_stamps: merge_lists' with reversed args;

diff -r 6490fc7b3eed -r fe218fdc961a src/Pure/sign.ML
--- 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 "