clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";
--- 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);