# HG changeset patch
# User wenzelm
# Date 1208268736 -7200
# Node ID 35249f5367b3145b5e5c974e2f54383cfb8dc48c
# Parent  62fff5feb75636f30ce6580e54691c3d3ef14fa8
merge: canonical order;

diff -r 62fff5feb756 -r 35249f5367b3 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Tue Apr 15 16:12:15 2008 +0200
+++ b/src/Pure/General/name_space.ML	Tue Apr 15 16:12:16 2008 +0200
@@ -202,20 +202,18 @@
 
 (* merge *)
 
-(* FIXME non-canonical merge order!? *)
-
 fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
   let
     val tab' = (tab1, tab2) |> Symtab.join
       (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
         if stamp1 = stamp2 then raise Symtab.SAME
         else
-          ((Library.merge (op =) (names2, names1),
-            Library.merge (op =) (names2', names1')), stamp ())));
+          ((Library.merge (op =) (names1, names2),
+            Library.merge (op =) (names1', names2')), stamp ())));
     val xtab' = (xtab1, xtab2) |> Symtab.join
       (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
         if stamp1 = stamp2 then raise Symtab.SAME
-        else (Library.merge (op =) (xnames2, xnames1), stamp ())));
+        else (Library.merge (op =) (xnames1, xnames2), stamp ())));
   in NameSpace (tab', xtab') end;