# HG changeset patch
# User wenzelm
# Date 1222183738 -7200
# Node ID 7c693bb763665ba6d217857e7f514d49b9c7c900
# Parent  507b64f4cd2a473438c805a295fd49421de2f93a
added fold_rev;
tuned dest, keys;

diff -r 507b64f4cd2a -r 7c693bb76366 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Tue Sep 23 15:48:55 2008 +0200
+++ b/src/Pure/General/table.ML	Tue Sep 23 17:28:58 2008 +0200
@@ -24,6 +24,7 @@
   val map: ('a -> 'b) -> 'a table -> 'b table
   val map': (key -> 'a -> 'b) -> 'a table -> 'b table
   val fold: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
+  val fold_rev: (key * 'b -> 'a -> 'a) -> 'b table -> 'a -> 'a
   val fold_map: (key * 'b -> 'a -> 'c * 'a) -> 'b table -> 'a -> 'c table * 'a
   val dest: 'a table -> (key * 'a) list
   val keys: 'a table -> key list
@@ -104,6 +105,15 @@
           fold right (f p2 (fold mid (f p1 (fold left x))));
   in fold end;
 
+fun fold_rev_table f =
+  let
+    fun fold Empty x = x
+      | fold (Branch2 (left, p, right)) x =
+          fold left (f p (fold right x))
+      | fold (Branch3 (left, p1, mid, p2, right)) x =
+          fold left (f p1 (fold mid (f p2 (fold right x))));
+  in fold end;
+
 fun fold_map_table f =
   let
     fun fold_map Empty s = (Empty, s)
@@ -123,8 +133,8 @@
           |-> (fn ((((l, e1), m), e2), r) => pair (Branch3 (l, (k1, e1), m, (k2, e2), r)))
   in fold_map end;
 
-fun dest tab = rev (fold_table cons tab []);
-fun keys tab = rev (fold_table (cons o #1) tab []);
+fun dest tab = fold_rev_table cons tab [];
+fun keys tab = fold_rev_table (cons o #1) tab [];
 
 fun get_first f tab =
   let
@@ -391,6 +401,7 @@
 fun map f = map_table (K f);
 val map' = map_table;
 val fold = fold_table;
+val fold_rev = fold_rev_table;
 val fold_map = fold_map_table;
 
 end;