diff -r 64aad1e46f98 -r 97ccf48c2f0c src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Fri Mar 27 13:04:15 2020 +0100
+++ b/src/Pure/General/graph.scala	Fri Mar 27 22:01:27 2020 +0100
@@ -123,9 +123,9 @@
     (Map.empty[Key, Long] /: xs)(reach(0))
   }
   def node_height(count: Key => Long): Map[Key, Long] =
-    reachable_length(count, imm_preds(_), maximals)
+    reachable_length(count, imm_preds, maximals)
   def node_depth(count: Key => Long): Map[Key, Long] =
-    reachable_length(count, imm_succs(_), minimals)
+    reachable_length(count, imm_succs, minimals)
 
   /*reachable nodes with size limit*/
   def reachable_limit(
@@ -138,7 +138,7 @@
     {
       val (n, rs) = res
       if (rs.contains(x)) res
-      else ((n + count(x), rs + x) /: next(x))(reach _)
+      else ((n + count(x), rs + x) /: next(x))(reach)
     }
 
     @tailrec def reachs(size: Long, rs: Keys, rest: List[Key]): Keys =