src/Pure/General/name_space.ML
changeset 16444 80c8f742c6fc
parent 16341 e573e5167eda
child 16848 1c8a5bb7c688
     1.1 --- a/src/Pure/General/name_space.ML	Fri Jun 17 18:33:28 2005 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Fri Jun 17 18:33:29 2005 +0200
     1.3 @@ -120,9 +120,8 @@
     1.4    | SOME (name :: _, _) => (name, false)
     1.5    | SOME ([], name' :: _) => (hidden name', true));
     1.6  
     1.7 -fun valid_accesses (NameSpace tab) name =
     1.8 -  ([], tab) |> Symtab.foldl (fn (accs, (xname, (names, _))) =>
     1.9 -    if null names orelse hd names <> name then accs else xname :: accs);
    1.10 +fun valid_accesses (NameSpace tab) name = Symtab.fold (fn (xname, (names, _)) =>
    1.11 +  if not (null names) andalso hd names = name then cons xname else I) tab [];
    1.12  
    1.13  
    1.14  (* intern and extern *)
    1.15 @@ -178,10 +177,9 @@
    1.16  
    1.17  (* merge *)
    1.18  
    1.19 -fun merge (NameSpace tab1, space2) = (space2, tab1) |> Symtab.foldl
    1.20 -  (fn (space, (xname, (names1, names1'))) =>
    1.21 -    map_space (fn (names2, names2') =>
    1.22 -      (merge_lists' names2 names1, merge_lists' names2' names1')) xname space);
    1.23 +fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
    1.24 +  xname |> map_space (fn (names2, names2') =>
    1.25 +    (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
    1.26  
    1.27  
    1.28  (* dest *)