diff -r 1d33697199c1 -r daca5f2a0c90 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Tue May 29 18:09:08 2018 +0200
+++ b/src/Pure/General/graph.scala	Tue May 29 20:00:10 2018 +0200
@@ -66,6 +66,7 @@
 
   def is_empty: Boolean = rep.isEmpty
   def defined(x: Key): Boolean = rep.isDefinedAt(x)
+  def domain: Set[Key] = rep.keySet
 
   def iterator: Iterator[(Key, Entry)] = rep.iterator