# HG changeset patch
# User wenzelm
# Date 894108426 -7200
# Node ID 31f23b8d6851333f9b0a8b1f503d4f7eaf988763
# Parent  54fa88124d5299bf52c10ae9a52df52c7aad964f
added accesses: string -> string list;

diff -r 54fa88124d52 -r 31f23b8d6851 src/Pure/name_space.ML
--- a/src/Pure/name_space.ML	Fri May 01 22:40:20 1998 +0200
+++ b/src/Pure/name_space.ML	Sat May 02 13:27:06 1998 +0200
@@ -17,6 +17,7 @@
   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
@@ -57,9 +58,7 @@
     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;
 
 
 
@@ -78,7 +77,7 @@
 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));