# HG changeset patch
# User wenzelm
# Date 1006795988 -3600
# Node ID 45269a593e1b82cc69b52828594d5920ee1626a7
# Parent  83f747db967cb677f4e2b680619e69ae656a4b13
clarified order of merge_lists';

diff -r 83f747db967c -r 45269a593e1b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Mon Nov 26 17:48:22 2001 +0100
+++ b/src/Pure/sign.ML	Mon Nov 26 18:33:08 2001 +0100
@@ -1086,7 +1086,7 @@
 (* merge_stamps *)
 
 fun merge_stamps stamps1 stamps2 =
-  let val stamps = merge_lists' stamps2 stamps1 in
+  let val stamps = merge_lists' stamps1 stamps2 in
     (case duplicates (map ! stamps) of
       [] => stamps
     | dups => raise TERM ("Attempt to merge different versions of theories "