src/Pure/General/graph.scala

--- a/src/Pure/General/graph.scala	Sun Sep 15 13:37:53 2019 +0200
+++ b/src/Pure/General/graph.scala	Sun Sep 15 13:42:01 2019 +0200
@@ -191,6 +191,8 @@
   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 */