src/Pure/General/name_space.ML

     (fn (entry, _) => (f entry, stamp ())) tab, xtab);
 
 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 =);
 
 end;
 

   else
     let val names = valid_accesses space name in
       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;
 
 
 (* merge *)