# HG changeset patch
# User wenzelm
# Date 1236282928 -3600
# Node ID f49d70426690303d226141b3383bc1854587c7e6
# Parent  b28caca9157f92f556df89d040a0afc6c0f6e46e
removed unused TableFun().fold_map and GraphFun().fold_map_nodes;

diff -r b28caca9157f -r f49d70426690 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Thu Mar 05 20:17:02 2009 +0100
+++ b/src/Pure/General/graph.ML	Thu Mar 05 20:55:28 2009 +0100
@@ -21,7 +21,6 @@
   val maximals: 'a T -> key list
   val subgraph: (key -> bool) -> 'a T -> 'a T
   val map_nodes: ('a -> 'b) -> 'a T -> 'b T
-  val fold_map_nodes: (key * 'a -> 'b -> 'c * 'b) -> 'a T -> 'b -> 'c T * 'b
   val get_node: 'a T -> key -> 'a                                     (*exception UNDEF*)
   val map_node: key -> ('a -> 'a) -> 'a T -> 'a T
   val map_node_yield: key -> ('a -> 'b * 'a) -> 'a T -> 'b * 'a T
@@ -116,9 +115,6 @@
 
 fun map_nodes f (Graph tab) = Graph (Table.map (fn (i, ps) => (f i, ps)) tab);
 
-fun fold_map_nodes f (Graph tab) =
-  apfst Graph o Table.fold_map (fn (k, (i, ps)) => f (k, i) #> apfst (rpair ps)) tab;
-
 fun get_node G = #1 o get_entry G;
 
 fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
diff -r b28caca9157f -r f49d70426690 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Mar 05 20:17:02 2009 +0100
+++ b/src/Pure/General/table.ML	Thu Mar 05 20:55:28 2009 +0100
@@ -24,7 +24,6 @@
   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
   val exists: (key * 'a -> bool) -> 'a table -> bool
@@ -112,25 +111,6 @@
           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)
-      | fold_map (Branch2 (left, p as (k, x), right)) s =
-          s
-          |> fold_map left
-          ||>> f p
-          ||>> fold_map right
-          |-> (fn ((l, e), r) => pair (Branch2 (l, (k, e), r)))
-      | fold_map (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) s =
-          s
-          |> fold_map left
-          ||>> f p1
-          ||>> fold_map mid
-          ||>> f p2
-          ||>> fold_map right
-          |-> (fn ((((l, e1), m), e2), r) => pair (Branch3 (l, (k1, e1), m, (k2, e2), r)))
-  in fold_map end;
-
 fun dest tab = fold_rev_table cons tab [];
 fun keys tab = fold_rev_table (cons o #1) tab [];
 
@@ -398,7 +378,6 @@
 val map' = map_table;
 val fold = fold_table;
 val fold_rev = fold_rev_table;
-val fold_map = fold_map_table;
 
 end;