diff -r b41d8e290bf8 -r 6cd180204582 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Sep 01 16:19:02 2005 +0200
+++ b/src/Pure/General/name_space.ML	Thu Sep 01 18:48:50 2005 +0200
@@ -113,7 +113,7 @@
 val empty = NameSpace Symtab.empty;
 
 fun lookup (NameSpace tab) xname =
-  (case Symtab.lookup (tab, xname) of
+  (case Symtab.curried_lookup tab xname of
     NONE => (xname, true)
   | SOME ([], []) => (xname, true)
   | SOME ([name], _) => (name, true)
@@ -150,7 +150,7 @@
 (* basic operations *)
 
 fun map_space f xname (NameSpace tab) =
-  NameSpace (Symtab.update ((xname, f (if_none (Symtab.lookup (tab, xname)) ([], []))), tab));
+  NameSpace (Symtab.curried_update (xname, f (if_none (Symtab.curried_lookup tab xname) ([], []))) tab);
 
 fun del (name: string) = remove (op =) name;
 fun add name names = name :: del name names;