# HG changeset patch
# User wenzelm
# Date 876239881 -7200
# Node ID 3e581526ae5eb1edff50317472da3b242e03c261
# Parent  f13d5b8408581d5dacd733f4b3ba8c61f63a1321
tuned internal mapping table;
improved merge: 2nd overrides 1st;

diff -r f13d5b840858 -r 3e581526ae5e src/Pure/name_space.ML
--- a/src/Pure/name_space.ML	Tue Oct 07 17:08:48 1997 +0200
+++ b/src/Pure/name_space.ML	Tue Oct 07 17:58:01 1997 +0200
@@ -10,6 +10,7 @@
 
 TODO:
   - absolute paths?
+  - also enter into parents!?
 *)
 
 signature NAME_SPACE =
@@ -82,7 +83,8 @@
       let val packed = pack entry in
         map (rpair packed o pack) (suffixes1 entry)
       end;
-    val mapping = gen_distinct eq_fst (flat (map accesses entries));
+    val mapping = filter_out (op =)
+      (gen_distinct eq_fst (flat (map accesses entries)));
   in
     NameSpace (entries, Symtab.make mapping)
   end;
@@ -98,8 +100,8 @@
 fun extend (entries, space) =
   make (map unpack (rev entries) @ entries_of space);
 
-fun merge (space1, space2) =
-  make (merge_lists (entries_of space1) (entries_of space2));
+fun merge (space1, space2) =    (*2nd overrides 1st*)
+  make (merge_lists (entries_of space2) (entries_of space1));
 
 
 (* lookup / prune names *)