exported get_accesses (for diagnostic purpose)
authorhaftmann
Mon Dec 01 12:17:01 2008 +0100 (2008-12-01)
changeset 289230a981c596372
parent 28922 ac2c34cad840
child 28924 5c8781b7d6a4
exported get_accesses (for diagnostic purpose)
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Mon Dec 01 12:17:00 2008 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Mon Dec 01 12:17:01 2008 +0100
     1.3 @@ -48,6 +48,7 @@
     1.4    val intern: T -> xstring -> string
     1.5    val extern: T -> string -> xstring
     1.6    val hide: bool -> string -> T -> T
     1.7 +  val get_accesses: T -> string -> xstring list
     1.8    val merge: T * T -> T
     1.9    type naming
    1.10    val path_of: naming -> string
    1.11 @@ -323,7 +324,6 @@
    1.12  fun declare_binding bnaming (Binding ((prefix, bname), _)) =
    1.13    let
    1.14      val naming = apply_prefix prefix bnaming;
    1.15 -    val dname = full bnaming bname;
    1.16      val name = full naming bname;
    1.17    in declare naming name #> pair name end;
    1.18