# 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;