src/Pure/General/name_space.ML
changeset 27196 ef2f01da7a12
parent 26657 35249f5367b3
child 28860 b1d46059d502
     1.1 --- a/src/Pure/General/name_space.ML	Fri Jun 13 21:04:42 2008 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Jun 13 21:04:43 2008 +0200
     1.3 @@ -179,6 +179,7 @@
     1.4  in
     1.5  
     1.6  val del_name = map_space o apfst o remove (op =);
     1.7 +fun del_name_extra name = map_space (apfst (fn [] => [] | x :: xs => x :: remove (op =) name xs));
     1.8  val add_name = map_space o apfst o update (op =);
     1.9  val add_name' = map_space o apsnd o update (op =);
    1.10  
    1.11 @@ -197,6 +198,7 @@
    1.12        space
    1.13        |> add_name' name name
    1.14        |> fold (del_name name) (if fully then names else names inter_string [base name])
    1.15 +      |> fold (del_name_extra name) (get_accesses space name)
    1.16      end;
    1.17  
    1.18