src/Pure/General/graph.ML

   val get_first: (key * ('a * (Keys.T * Keys.T)) -> 'b option) -> 'a T -> 'b option
   val fold: (key * ('a * (Keys.T * Keys.T)) -> 'b -> 'b) -> 'a T -> 'b -> 'b
   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
   val immediate_preds: 'a T -> key -> key list
   val immediate_succs: 'a T -> key -> key list

     SOME entry => entry
   | NONE => raise UNDEF x);
 
 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 *)
 
 fun get_node G = #1 o #2 o get_entry G;
 
 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);
 
 
 (* reachability *)