# HG changeset patch
# User wenzelm
# Date 1267572813 -3600
# Node ID b8863ee98f568e90a02886bdf1da624fad356770
# Parent  8758fe1fc9f8b7b1e5cdd13237b77f0ea37c7ab7
removed unused external_names;

diff -r 8758fe1fc9f8 -r b8863ee98f56 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 *)