# HG changeset patch
# User berghofe
# Date 1064240386 -7200
# Node ID 8ea2645b813231fdba312c2ee188667f490e8d03
# Parent  3d7c6fc7c66e3fed35313c3a1641b3c08db43255
Modified merge_aux to prevent newer names from getting overwritten
by older names.

diff -r 3d7c6fc7c66e -r 8ea2645b8132 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Sep 22 16:16:03 2003 +0200
+++ b/src/Pure/General/name_space.ML	Mon Sep 22 16:19:46 2003 +0200
@@ -106,8 +106,9 @@
 
 (* merge *)             (*1st preferred over 2nd*)
 
-fun merge_aux (tab, (xname, (names, names'))) =
-  foldr (change add xname) (names, foldr (change' add xname) (names', tab));
+fun merge_aux (tab, (xname, (names1, names1'))) =
+  map_space (fn (names2, names2') =>
+    (merge_lists' names2 names1, merge_lists' names2' names1')) xname tab;
 
 fun merge (NameSpace tab1, NameSpace tab2) =
   NameSpace (Symtab.foldl merge_aux (tab2, tab1));