src/Pure/General/name_space.ML
changeset 16002 e0557c452138
parent 15624 484178635bd8
child 16137 00e9ca1e7261
     1.1 --- a/src/Pure/General/name_space.ML	Wed May 18 11:30:58 2005 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Wed May 18 11:30:59 2005 +0200
     1.3 @@ -76,7 +76,7 @@
     1.4  (* basic operations *)
     1.5  
     1.6  fun map_space f xname tab =
     1.7 -  Symtab.update ((xname, f (getOpt (Symtab.lookup (tab, xname), ([], [])))), tab);
     1.8 +  Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab);
     1.9  
    1.10  fun change f xname (name, tab) =
    1.11    map_space (fn (names, names') => (f names name, names')) xname tab;