# HG changeset patch
# User haftmann
# Date 1228130221 -3600
# Node ID 0a981c596372b66b65aa7677994196a4f01f74c3
# Parent  ac2c34cad840b953a4791ee36de0bafa5d725b02
exported get_accesses (for diagnostic purpose)

diff -r ac2c34cad840 -r 0a981c596372 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Mon Dec 01 12:17:00 2008 +0100
+++ b/src/Pure/General/name_space.ML	Mon Dec 01 12:17:01 2008 +0100
@@ -48,6 +48,7 @@
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val hide: bool -> string -> T -> T
+  val get_accesses: T -> string -> xstring list
   val merge: T * T -> T
   type naming
   val path_of: naming -> string
@@ -323,7 +324,6 @@
 fun declare_binding bnaming (Binding ((prefix, bname), _)) =
   let
     val naming = apply_prefix prefix bnaming;
-    val dname = full bnaming bname;
     val name = full naming bname;
   in declare naming name #> pair name end;