added del_node, which is more efficient for sparse graphs;

--- a/src/Pure/General/graph.ML	Tue Sep 23 15:48:54 2008 +0200
+++ b/src/Pure/General/graph.ML	Tue Sep 23 15:48:55 2008 +0200
@@ -34,6 +34,7 @@
   val new_node: key * 'a -> 'a T -> 'a T                              (*exception DUP*)
   val default_node: key * 'a -> 'a T -> 'a T
   val del_nodes: key list -> 'a T -> 'a T                             (*exception UNDEF*)
+  val del_node: key -> 'a T -> 'a T                                   (*exception UNDEF*)
   val is_edge: 'a T -> key * key -> bool
   val add_edge: key * key -> 'a T -> 'a T
   val del_edge: key * key -> 'a T -> 'a T
@@ -165,6 +166,17 @@
     |> Table.map (fn (i, (preds, succs)) =>
       (i, (fold remove_key xs preds, fold remove_key xs succs))));
 
+fun del_node x (G as Graph tab) =
+  let
+    fun del_adjacent which y = Table.map_entry y (fn (i, ps) => (i, (which (remove_key x) ps)));
+    val (preds, succs) = #2 (get_entry G x);
+  in
+    Graph (tab
+      |> Table.delete x
+      |> fold (del_adjacent apsnd) preds
+      |> fold (del_adjacent apfst) succs)
+  end;
+
 
 (* edges *)