src/Pure/General/name_space.ML
changeset 18939 18e2a2676d80
parent 18011 685d95c793ff
child 19015 1075db658d91
     1.1 --- a/src/Pure/General/name_space.ML	Mon Feb 06 20:59:05 2006 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Feb 06 20:59:06 2006 +0100
     1.3 @@ -150,7 +150,7 @@
     1.4  (* basic operations *)
     1.5  
     1.6  fun map_space f xname (NameSpace tab) =
     1.7 -  NameSpace (Symtab.update (xname, f (if_none (Symtab.lookup tab xname) ([], []))) tab);
     1.8 +  NameSpace (Symtab.update (xname, f (the_default ([], []) (Symtab.lookup tab xname))) tab);
     1.9  
    1.10  fun del (name: string) = remove (op =) name;
    1.11  fun add name names = name :: del name names;
    1.12 @@ -179,7 +179,7 @@
    1.13  
    1.14  fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
    1.15    xname |> map_space (fn (names2, names2') =>
    1.16 -    (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
    1.17 +    (Library.merge (op =) (names2, names1), Library.merge (op =) (names2', names1')))) tab1 space2;
    1.18  
    1.19  
    1.20