--- a/src/Pure/General/name_space.ML Sun Aug 28 16:04:46 2005 +0200
+++ b/src/Pure/General/name_space.ML Sun Aug 28 16:04:47 2005 +0200
@@ -39,7 +39,6 @@
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
@@ -183,16 +182,6 @@
(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 **)