hide: delete all accesses from extra names -- reduces ambiguity in extern;

--- a/src/Pure/General/name_space.ML	Fri Jun 13 21:04:42 2008 +0200
+++ b/src/Pure/General/name_space.ML	Fri Jun 13 21:04:43 2008 +0200
@@ -179,6 +179,7 @@
 in
 
 val del_name = map_space o apfst o remove (op =);
+fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
 val add_name = map_space o apfst o update (op =);
 val add_name' = map_space o apsnd o update (op =);
 
@@ -197,6 +198,7 @@
       space
       |> add_name' name name
       |> fold (del_name name) (if fully then names else names inter_string [base name])
+      |> fold (del_name_extra name) (get_accesses space name)
     end;