# HG changeset patch
# User wenzelm
# Date 1431537179 -7200
# Node ID 014b86186c49a5f7f2f1d707e0265caa8a486015
# Parent  c927fa99d045b184e75aa08f385c6a32fe423a9b
clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";

diff -r c927fa99d045 -r 014b86186c49 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed May 13 17:36:33 2015 +0200
+++ b/src/Pure/General/name_space.ML	Wed May 13 19:12:59 2015 +0200
@@ -450,8 +450,7 @@
       val (accs, accs') = accesses naming binding;
       val internals' = internals |> fold (add_name name) accs;
       val entries' = entries
-        |> Change_Table.map_entry name (fn (externals, entry) =>
-          (Library.merge (op =) (externals, accs'), entry))
+        |> Change_Table.map_entry name (apfst (fold_rev (update op =) accs'));
     in (kind, internals', entries') end);