--- a/src/Pure/General/graph.ML Sat Feb 25 13:13:14 2012 +0100
+++ b/src/Pure/General/graph.ML Sat Feb 25 13:17:38 2012 +0100
@@ -174,7 +174,7 @@
fun is_maximal G x = Keys.is_empty (imm_succs G x);
-(* nodes *)
+(* node operations *)
fun new_node (x, info) (Graph tab) =
Graph (Table.update_new (x, (info, (Keys.empty, Keys.empty))) tab);
@@ -198,7 +198,7 @@
fold_graph (fn (x, _) => not (pred x) ? del_node x) G G;
-(* edges *)
+(* edge operations *)
fun is_edge G (x, y) = Keys.member (imm_succs G x) y handle UNDEF _ => false;