src/Pure/General/name_space.ML
changeset 17221 6cd180204582
parent 17163 f1455d56e5b5
child 17412 e26cb20ef0cc
     1.1 --- a/src/Pure/General/name_space.ML	Thu Sep 01 16:19:02 2005 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Sep 01 18:48:50 2005 +0200
     1.3 @@ -113,7 +113,7 @@
     1.4  val empty = NameSpace Symtab.empty;
     1.5  
     1.6  fun lookup (NameSpace tab) xname =
     1.7 -  (case Symtab.lookup (tab, xname) of
     1.8 +  (case Symtab.curried_lookup tab xname of
     1.9      NONE => (xname, true)
    1.10    | SOME ([], []) => (xname, true)
    1.11    | SOME ([name], _) => (name, true)
    1.12 @@ -150,7 +150,7 @@
    1.13  (* basic operations *)
    1.14  
    1.15  fun map_space f xname (NameSpace tab) =
    1.16 -  NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab));
    1.17 +  NameSpace (Symtab.curried_update (xname, f (if_none (Symtab.curried_lookup tab xname) ([], []))) tab);
    1.18  
    1.19  fun del (name: string) = remove (op =) name;
    1.20  fun add name names = name :: del name names;