src/Pure/General/name_space.ML
changeset 30213 3951aab916fd
parent 29848 a7c164e228e1
child 30215 47cce3d47e62
     1.1 --- a/src/Pure/General/name_space.ML	Tue Mar 03 14:08:53 2009 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Tue Mar 03 14:16:05 2009 +0100
     1.3 @@ -133,19 +133,10 @@
     1.4    | SOME ((name :: _, _), _) => (name, false)
     1.5    | SOME (([], name' :: _), _) => (hidden name', true));
     1.6  
     1.7 -fun ex_mapsto_in (NameSpace (tab, _)) name xname =
     1.8 -    (case Symtab.lookup tab xname of
     1.9 -      SOME ((name'::_, _), _) => name' = name
    1.10 -    | _ => false);
    1.11 -
    1.12 -fun get_accesses' valid_only (ns as (NameSpace (_, tab))) name =
    1.13 +fun get_accesses (NameSpace (_, tab)) name =
    1.14    (case Symtab.lookup tab name of
    1.15      NONE => [name]
    1.16 -  | SOME (xnames, _) => if valid_only
    1.17 -                        then filter (ex_mapsto_in ns name) xnames
    1.18 -                        else xnames);
    1.19 -
    1.20 -val get_accesses = get_accesses' true;
    1.21 +  | SOME (xnames, _) => xnames);
    1.22  
    1.23  fun put_accesses name xnames (NameSpace (tab, xtab)) =
    1.24    NameSpace (tab, Symtab.update (name, (xnames, stamp ())) xtab);
    1.25 @@ -169,7 +160,7 @@
    1.26    in
    1.27      if ! long_names then name
    1.28      else if ! short_names then base name
    1.29 -    else ext (get_accesses' false space name)
    1.30 +    else ext (get_accesses space name)
    1.31    end;
    1.32  
    1.33  
    1.34 @@ -203,7 +194,7 @@
    1.35        space
    1.36        |> add_name' name name
    1.37        |> fold (del_name name) (if fully then names else names inter_string [base name])
    1.38 -      |> fold (del_name_extra name) (get_accesses' false space name)
    1.39 +      |> fold (del_name_extra name) (get_accesses space name)
    1.40      end;
    1.41  
    1.42