adapted Binding.dest;
tuned;

--- a/src/Pure/General/name_space.ML	Thu Mar 05 10:52:07 2009 +0100
+++ b/src/Pure/General/name_space.ML	Thu Mar 05 10:53:49 2009 +0100
@@ -123,7 +123,7 @@
 datatype T =
   NameSpace of
     (string list * string list) Symtab.table *   (*internals, hidden internals*)
-    string list Symtab.table;                    (*externals*)
+    xstring list Symtab.table;                   (*externals*)
 
 val empty = NameSpace (Symtab.empty, Symtab.empty);
 
@@ -153,9 +153,9 @@
 
 fun extern_flags {long_names, short_names, unique_names} space name =
   let
-    fun valid unique xname =
-      let val (name', uniq) = lookup space xname
-      in name = name' andalso (uniq orelse not unique) end;
+    fun valid require_unique xname =
+      let val (name', is_unique) = lookup space xname
+      in name = name' andalso (not require_unique orelse is_unique) end;
 
     fun ext [] = if valid false name then name else hidden name
       | ext (nm :: nms) = if valid unique_names nm then nm else ext nms;
@@ -278,8 +278,8 @@
 
 fun full_name naming binding =
   let
-    val (prefix, qualifier, bname) = Binding.dest binding;
-    val naming' = apply_prefix (prefix @ qualifier) naming;
+    val (prfx, bname) = Binding.dest binding;
+    val naming' = apply_prefix prfx naming;
   in full naming' bname end;
 
 
@@ -287,8 +287,8 @@
 
 fun declare naming binding space =
   let
-    val (prefix, qualifier, bname) = Binding.dest binding;
-    val naming' = apply_prefix (prefix @ qualifier) naming;
+    val (prfx, bname) = Binding.dest binding;
+    val naming' = apply_prefix prfx naming;
     val name = full naming' bname;
     val names = explode_name name;