added dest_table;
authorwenzelm
Thu Jul 14 19:28:32 2005 +0200 (2005-07-14)
changeset 168481c8a5bb7c688
parent 16847 8fc160b12e73
child 16849 a6cdb1ade955
added dest_table;
src/Pure/General/name_space.ML
     1.1 --- a/src/Pure/General/name_space.ML	Thu Jul 14 19:28:31 2005 +0200
     1.2 +++ b/src/Pure/General/name_space.ML	Thu Jul 14 19:28:32 2005 +0200
     1.3 @@ -55,6 +55,7 @@
     1.4    val empty_table: 'a table
     1.5    val extend_table: naming -> 'a table * (bstring * 'a) list -> 'a table
     1.6    val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table
     1.7 +  val dest_table: 'a table -> (string * 'a) list
     1.8    val extern_table: 'a table -> (xstring * 'a) list
     1.9  end;
    1.10  
    1.11 @@ -257,8 +258,12 @@
    1.12  fun merge_tables eq ((space1, tab1), (space2, tab2)) =
    1.13    (merge (space1, space2), (Symtab.merge eq (tab1, tab2)));
    1.14  
    1.15 -fun extern_table (space, tab) =
    1.16 -  Library.sort_wrt #1 (map (apfst (extern space)) (Symtab.dest tab));
    1.17 +fun ext_table (space, tab) =
    1.18 +  Symtab.fold (fn (name, x) => cons ((name, extern space name), x)) tab []
    1.19 +  |> Library.sort_wrt (#2 o #1);
    1.20 +
    1.21 +fun dest_table tab = map (apfst #1) (ext_table tab);
    1.22 +fun extern_table tab = map (apfst #2) (ext_table tab);
    1.23  
    1.24  end;
    1.25