# HG changeset patch
# User wenzelm
# Date 1144764006 -7200
# Node ID 28bf2447c1807649ae4de894f2ec9524f9d87ab4
# Parent  9a52d5b7fc274650d6db2b61b02cb7f96e5bb735
tuned;

diff -r 9a52d5b7fc27 -r 28bf2447c180 src/Pure/General/graph.ML
--- 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;