merge_stamps: merge_lists' with reversed args;
authorwenzelm
Sat Nov 24 16:57:34 2001 +0100 (2001-11-24)
changeset 12286fe218fdc961a
parent 12285 6490fc7b3eed
child 12287 7017cee2f3ac
merge_stamps: merge_lists' with reversed args;
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Sat Nov 24 16:56:26 2001 +0100
     1.2 +++ b/src/Pure/sign.ML	Sat Nov 24 16:57:34 2001 +0100
     1.3 @@ -1086,7 +1086,7 @@
     1.4  (* merge_stamps *)
     1.5  
     1.6  fun merge_stamps stamps1 stamps2 =
     1.7 -  let val stamps = merge_rev_lists stamps1 stamps2 in
     1.8 +  let val stamps = merge_lists' stamps2 stamps1 in
     1.9      (case duplicates (map ! stamps) of
    1.10        [] => stamps
    1.11      | dups => raise TERM ("Attempt to merge different versions of theories "