merge: canonical order;
authorwenzelm
Tue Apr 15 16:12:16 2008 +0200 (2008-04-15)
changeset 2665735249f5367b3
parent 26656 62fff5feb756
child 26658 5967c2a0a94f
merge: canonical order;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Tue Apr 15 16:12:15 2008 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Apr 15 16:12:16 2008 +0200
     1.3 @@ -202,20 +202,18 @@
     1.4  
     1.5  (* merge *)
     1.6  
     1.7 -(* FIXME non-canonical merge order!? *)
     1.8 -
     1.9  fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
    1.10    let
    1.11      val tab' = (tab1, tab2) |> Symtab.join
    1.12        (K (fn (((names1, names1'), stamp1), ((names2, names2'), stamp2)) =>
    1.13          if stamp1 = stamp2 then raise Symtab.SAME
    1.14          else
    1.15 -          ((Library.merge (op =) (names2, names1),
    1.16 -            Library.merge (op =) (names2', names1')), stamp ())));
    1.17 +          ((Library.merge (op =) (names1, names2),
    1.18 +            Library.merge (op =) (names1', names2')), stamp ())));
    1.19      val xtab' = (xtab1, xtab2) |> Symtab.join
    1.20        (K (fn ((xnames1, stamp1), (xnames2, stamp2)) =>
    1.21          if stamp1 = stamp2 then raise Symtab.SAME
    1.22 -        else (Library.merge (op =) (xnames2, xnames1), stamp ())));
    1.23 +        else (Library.merge (op =) (xnames1, xnames2), stamp ())));
    1.24    in NameSpace (tab', xtab') end;
    1.25  
    1.26