src/Pure/ML/ml_heap.scala

 
   def read_file_digest(heap: Path): Option[SHA1.Digest] = {
     if (heap.is_file) {
       val l = sha1_prefix.length
       val m = l + SHA1.digest_length
-      val n = heap.file.length
+      val n = File.size(heap)
       val bs = Bytes.read_file(heap, offset = n - m)
       if (bs.length == m) {
         val s = bs.text
         if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l)))
         else None