tuned;

--- a/src/Pure/General/graph.ML	Tue Apr 11 16:00:05 2006 +0200
+++ b/src/Pure/General/graph.ML	Tue Apr 11 16:00:06 2006 +0200
@@ -144,10 +144,8 @@
 fun subgraph keys (Graph tab) =
   let
     val select = member eq_key keys;
-    fun subg (k, (i, (preds, succs))) tab' =
-      if select k
-      then tab' |> Table.update (k, (i, (filter select preds, filter select succs)))
-      else tab'
+    fun subg (k, (i, (preds, succs))) =
+      K (select k) ? Table.update (k, (i, (filter select preds, filter select succs)));
   in Table.empty |> Table.fold subg tab |> Graph end;