# HG changeset patch
# User wenzelm
# Date 1026305268 -7200
# Node ID f130bcf2962078bd9aa1c93a5cef4f18747fcb1f
# Parent  47e9950a502d650a5cfe4fb33a2695d90deb2cce
added accesses';

diff -r 47e9950a502d -r f130bcf29620 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Wed Jul 10 13:55:32 2002 +0200
+++ b/src/Pure/General/name_space.ML	Wed Jul 10 14:47:48 2002 +0200
@@ -21,6 +21,7 @@
   val map_base: (string -> string) -> string -> string
   val is_qualified: string -> bool
   val accesses: string -> string list
+  val accesses': string -> string list
   type T
   val empty: T
   val extend: T * string list -> T
@@ -64,6 +65,8 @@
     val pfxs = map (fn x => x @ [b]) (Library.prefixes1 q);
   in map pack (sfxs @ pfxs) end;
 
+val accesses' = map pack o Library.suffixes1 o unpack;
+
 
 
 (** name spaces **)
@@ -142,7 +145,7 @@
       | try (nm :: nms) =
           let val (full_nm, uniq) = lookup space nm
           in if full_nm = name andalso uniq then nm else try nms end
-  in try (map pack (Library.suffixes1 (unpack name))) end;
+  in try (accesses' name) end;
 
 (*prune names on output by default*)
 val long_names = ref false;