src/Pure/Thy/store.scala
changeset 78182 31835adf148a
parent 78181 c2fbe48e9df4
child 78184 4309bcc8f28b
--- a/src/Pure/Thy/store.scala	Tue Jun 20 16:48:47 2023 +0200
+++ b/src/Pure/Thy/store.scala	Tue Jun 20 18:23:17 2023 +0200
@@ -230,7 +230,7 @@
   def find_heap_shasum(name: String): SHA1.Shasum =
     (for {
       path <- find_heap(name)
-      digest <- ML_Heap.read_digest(path)
+      digest <- ML_Heap.read_file_digest(path)
     } yield SHA1.shasum(digest, name)).getOrElse(SHA1.no_shasum)
 
   def the_heap(name: String): Path =