--- a/src/Pure/General/graph.ML Sun Jan 26 16:23:46 2014 +0100
+++ b/src/Pure/General/graph.ML Sun Jan 26 16:23:47 2014 +0100
@@ -27,7 +27,6 @@
val get_entry: 'a T -> key -> key * ('a * (Keys.T * Keys.T)) (*exception UNDEF*)
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
val map: (key -> 'a -> 'b) -> 'a T -> 'b T
val imm_preds: 'a T -> key -> Keys.T
val imm_succs: 'a T -> key -> Keys.T
@@ -122,10 +121,6 @@
fun map_entry x f (G as Graph tab) = Graph (Table.update (x, f (#2 (get_entry G x))) tab);
-fun map_entry_yield x f (G as Graph tab) =
- let val (a, node') = f (#2 (get_entry G x))
- in (a, Graph (Table.update (x, node') tab)) end;
-
(* nodes *)
@@ -133,9 +128,6 @@
fun map_node x f = map_entry x (fn (i, ps) => (f i, ps));
-fun map_node_yield x f = map_entry_yield x (fn (i, ps) =>
- let val (a, i') = f i in (a, (i', ps)) end);
-
fun map_nodes f (Graph tab) = Graph (Table.map (apfst o f) tab);