src/Pure/General/graph.scala

--- a/src/Pure/General/graph.scala	Thu Feb 23 15:15:59 2012 +0100
+++ b/src/Pure/General/graph.scala	Thu Feb 23 15:49:40 2012 +0100
@@ -146,6 +146,9 @@
       (((rep - x) /: preds)(del_adjacent(false, x)) /: succs)(del_adjacent(true, x)))
   }
 
+  def restrict(pred: Key => Boolean): Graph[Key, A] =
+    (this /: iterator){ case (graph, (x, _)) => if (!pred(x)) graph.del_node(x) else graph }
+
 
   /* edges */