# HG changeset patch
# User wenzelm
# Date 1125237887 -7200
# Node ID f1455d56e5b516378eefe7b5310917dc1780de4e
# Parent  c332aaf1b46011c5fb70b83d1f19639f072c9d53
removed unused dest operation;

diff -r c332aaf1b460 -r f1455d56e5b5 src/Pure/General/name_space.ML
--- 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 **)