diff -r 5baca4c94737 -r 3b50269b90c2 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Tue Oct 10 11:24:35 2017 +0200
+++ b/src/Pure/General/graph.scala	Tue Oct 10 13:46:12 2017 +0200
@@ -147,6 +147,8 @@
   def is_minimal(x: Key): Boolean = imm_preds(x).isEmpty
   def is_maximal(x: Key): Boolean = imm_succs(x).isEmpty
 
+  def is_isolated(x: Key): Boolean = is_minimal(x) && is_maximal(x)
+
 
   /* node operations */