clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";
authorwenzelm
Wed, 13 May 2015 19:12:59 +0200
changeset 60284 014b86186c49
parent 60283 c927fa99d045
child 60285 b4f1a0a701ae
clarified alias: proper update of new accesses instead of conservative insert (via merge), otherwise "local.foo" could take precedence over "foo";
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);