diff -r 5892fdda22c9 -r bc1e27bcc195 src/Pure/General/graph.ML
--- a/src/Pure/General/graph.ML	Sun Jan 24 11:33:54 1999 +0100
+++ b/src/Pure/General/graph.ML	Mon Jan 25 20:35:19 1999 +0100
@@ -21,11 +21,11 @@
   val all_succs: 'a T -> key list -> key list
   val find_paths: 'a T -> key * key -> key list list
   exception DUPLICATE of key
-  val add_node: key * 'a -> 'a T -> 'a T
+  val new_node: key * 'a -> 'a T -> 'a T
   val add_edge: key * key -> 'a T -> 'a T
+  val del_edge: key * key -> 'a T -> 'a T
   exception CYCLES of key list list
   val add_edge_acyclic: key * key -> 'a T -> 'a T
-  val derive_node: key * 'a -> key list -> 'a T -> 'a T
 end;
 
 functor GraphFun(Key: KEY): GRAPH =
@@ -44,6 +44,9 @@
 infix ins_key;
 val op ins_key = gen_ins eq_key;
 
+infix del_key;
+fun xs del_key x = if x mem_key xs then gen_rem eq_key (xs, x) else xs;
+
 
 (* tables and sets of keys *)
 
@@ -123,13 +126,19 @@
 
 exception DUPLICATE of key;
 
-fun add_node (x, info) (Graph tab) =
+fun new_node (x, info) (Graph tab) =
   Graph (Table.update_new ((x, (info, ([], []))), tab)
     handle Table.DUP key => raise DUPLICATE key);
 
-fun add_edge (x, y) G =
-  G |> map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs)))
-    |> map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs)));
+
+fun add_edge (x, y) =
+  map_entry x (fn (i, (preds, succs)) => (i, (preds, y ins_key succs))) o
+   map_entry y (fn (i, (preds, succs)) => (i, (x ins_key preds, succs)));
+
+fun del_edge (x, y) =
+  map_entry x (fn (i, (preds, succs)) => (i, (preds, succs del_key y))) o
+   map_entry y (fn (i, (preds, succs)) => (i, (preds del_key x, succs)));
+
 
 exception CYCLES of key list list;
 
@@ -138,9 +147,6 @@
     [] => add_edge (x, y) G
   | cycles => raise CYCLES (map (cons x) cycles));
 
-fun derive_node (x, y) zs G =
-  foldl (fn (H, z) => add_edge_acyclic (z, x) H) (add_node (x, y) G, zs);
-
 
 end;