# HG changeset patch
# User wenzelm
# Date 1121362112 -7200
# Node ID 1c8a5bb7c6880955322807c310b735c8d7e01eb4
# Parent  8fc160b12e73e74e82685b2d7b730c6d5f7b56b8
added dest_table;

diff -r 8fc160b12e73 -r 1c8a5bb7c688 src/Pure/General/name_space.ML
--- a/src/Pure/General/name_space.ML	Thu Jul 14 19:28:31 2005 +0200
+++ b/src/Pure/General/name_space.ML	Thu Jul 14 19:28:32 2005 +0200
@@ -55,6 +55,7 @@
   val empty_table: 'a table
   val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
   val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
+  val dest_table: 'a table -> (string * 'a) list
   val extern_table: 'a table -> (xstring * 'a) list
 end;
 
@@ -257,8 +258,12 @@
 fun merge_tables eq ((space1, tab1), (space2, tab2)) =
   (merge (space1, space2), (Symtab.merge eq (tab1, tab2)));
 
-fun extern_table (space, tab) =
-  Library.sort_wrt #1 (map (apfst (extern space)) (Symtab.dest tab));
+fun ext_table (space, tab) =
+  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
+  |> Library.sort_wrt (#2 o #1);
+
+fun dest_table tab = map (apfst #1) (ext_table tab);
+fun extern_table tab = map (apfst #2) (ext_table tab);
 
 end;