# HG changeset patch
# User wenzelm
# Date 883402238 -3600
# Node ID 2ba0730672c940c9c3a089d5a257de4fdd55aae5
# Parent  16187138463da2d3b0520f74e1d8d673d0fef7cf
removed declared;
improved dest;

diff -r 16187138463d -r 2ba0730672c9 src/Pure/name_space.ML
--- a/src/Pure/name_space.ML	Mon Dec 29 14:29:34 1997 +0100
+++ b/src/Pure/name_space.ML	Mon Dec 29 14:30:38 1997 +0100
@@ -17,13 +17,12 @@
   val base: string -> string
   val qualified: string -> bool
   type T
-  val dest: T -> string list
   val empty: T
-  val declared: T -> string -> bool
   val extend: T * string list -> T
   val merge: T * T -> T
   val intern: T -> string -> string
   val extern: T -> string -> string
+  val dest: T -> (string * string list) list
 end;
 
 structure NameSpace: NAME_SPACE =
@@ -70,13 +69,6 @@
 
 val empty = NameSpace Symtab.empty;
 
-(* FIXME !? *)
-fun dest (NameSpace tab) = map (fn (x, y) => x ^ " -> " ^ y) (Symtab.dest tab);
-fun dest (NameSpace tab) = map fst (Symtab.dest tab);
-
-(* FIXME !? *)
-fun declared (NameSpace tab) name = is_some (Symtab.lookup (tab, name));
-
 
 (* extend, merge operations *)
 
@@ -103,4 +95,11 @@
   in try (map pack (suffixes1 (unpack name))) end;
 
 
+(* dest *)
+
+fun dest (NameSpace tab) =
+  map (apsnd (sort (int_ord o pairself size)))
+    (Symtab.dest (Symtab.make_multi (map swap (Symtab.dest tab))));
+
+
 end;