src/Pure/General/name_space.ML

   val valid_accesses: T -> string -> xstring list
   val intern: T -> xstring -> string
   val extern: T -> string -> xstring
   val hide: bool -> string -> T -> T
   val merge: T * T -> T
-  val dest: T -> (string * xstring list) list
   type naming
   val path_of: naming -> string
   val full: naming -> bstring -> string
   val declare: naming -> string -> T -> T
   val default_naming: naming

 fun merge (NameSpace tab1, space2) = Symtab.fold (fn (xname, (names1, names1')) =>
   xname |> map_space (fn (names2, names2') =>
     (merge_lists' names2 names1, merge_lists' names2' names1'))) tab1 space2;
 
 
-(* dest *)
-
-fun dest_entry (xname, ([], _)) = NONE
-  | dest_entry (xname, (name :: _, _)) = SOME (name, xname);
-
-fun dest (NameSpace tab) =
-  map (apsnd (sort (int_ord o pairself size)))
-    (Symtab.dest (Symtab.make_multi (List.mapPartial dest_entry (Symtab.dest tab))));
-
-
 
 (** naming contexts **)
 
 (* datatype naming *)