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