--- 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;