src/Pure/General/graph.scala

--- a/src/Pure/General/graph.scala	Mon Jun 25 14:06:50 2018 +0100
+++ b/src/Pure/General/graph.scala	Mon Jun 25 17:18:55 2018 +0200
@@ -68,6 +68,7 @@
   def defined(x: Key): Boolean = rep.isDefinedAt(x)
   def domain: Set[Key] = rep.keySet
 
+  def size: Int = rep.size
   def iterator: Iterator[(Key, Entry)] = rep.iterator
 
   def keys_iterator: Iterator[Key] = iterator.map(_._1)