# HG changeset patch
# User haftmann
# Date 1390749827 -3600
# Node ID 2733a57d100f5df99856ee2d9d3dc4761f4f67ef
# Parent  eedd549de3ef5938a916f0f24121815a1af7f6f0
obsolete

diff -r eedd549de3ef -r 2733a57d100f src/Pure/General/graph.ML
--- 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);