src/Pure/name_space.ML

   val append: string -> string -> string
   val unpack: string -> string list
   val pack: string list -> string
   val base: string -> string
   val qualified: string -> bool
+  val accesses: string -> string list
   type T
   val empty: T
   val extend: T * string list -> T
   val merge: T * T -> T
   val intern: T -> string -> string

   let
     val uname = unpack name;
     val (q, b) = split_last uname;
     val sfxs = suffixes1 uname;
     val pfxs = map (fn x => x @ [b]) (prefixes1 q);
-  in
-    map (rpair name o pack) (sfxs @ pfxs)
-  end;
+  in map pack (sfxs @ pfxs) end;
 
 
 
 (** name spaces **)
 

 (* extend, merge operations *)
 
 fun add (tab, entry) = Symtab.update (entry, tab);
 
 fun extend (NameSpace tab, names) =
-  NameSpace (foldl add (tab, flat (map accesses names)));
+  NameSpace (foldl add (tab, flat (map (fn name => map (rpair name) (accesses name)) names)));
 
 fun merge (NameSpace tab1, NameSpace tab2) =    (*2nd overrides 1st*)
   NameSpace (foldl add (tab1, Symtab.dest tab2));