removed unused external_names;
authorwenzelm
Wed Mar 03 00:33:33 2010 +0100 (2010-03-03)
changeset 35432b8863ee98f56
parent 35431 8758fe1fc9f8
child 35433 73cc288b4f83
removed unused external_names;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Wed Mar 03 00:33:02 2010 +0100
     1.2 +++ b/src/Pure/General/name_space.ML	Wed Mar 03 00:33:33 2010 +0100
     1.3 @@ -46,7 +46,6 @@
     1.4    val qualified_path: bool -> binding -> naming -> naming
     1.5    val transform_binding: naming -> binding -> binding
     1.6    val full_name: naming -> binding -> string
     1.7 -  val external_names: naming -> string -> string list
     1.8    val declare: bool -> naming -> binding -> T -> string * T
     1.9    type 'a table = T * 'a Symtab.table
    1.10    val define: bool -> naming -> binding * 'a -> 'a table -> string * 'a table
    1.11 @@ -309,8 +308,6 @@
    1.12      val pfxs = mandatory_prefixes spec;
    1.13    in pairself (map Long_Name.implode) (sfxs @ pfxs, sfxs) end;
    1.14  
    1.15 -fun external_names naming = #2 o accesses naming o Binding.qualified_name;
    1.16 -
    1.17  
    1.18  (* declaration *)
    1.19