hide: delete all accesses from extra names -- reduces ambiguity in extern;
authorwenzelm
Fri Jun 13 21:04:43 2008 +0200 (2008-06-13)
changeset 27196ef2f01da7a12
parent 27195 bbf4cbc69243
child 27197 d1b8b6938b23
hide: delete all accesses from extra names -- reduces ambiguity in extern;
src/Pure/General/name_space.ML
     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