src/Pure/General/graph.scala

       (((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 }
+
+  def exclude(pred: Key => Boolean): Graph[Key, A] = restrict(name => !pred(name))
 
 
   /* edge operations */
 
   def edges_iterator: Iterator[(Key, Key)] =