src/Pure/ML/ml_heap.scala

--- a/src/Pure/ML/ml_heap.scala	Wed Jun 21 15:41:18 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Wed Jun 21 15:53:38 2023 +0200
@@ -111,7 +111,7 @@
   def clean_entry(db: SQL.Database, name: String): Unit =
     Data.transaction_lock(db, create = true) { Data.clean_entry(db, name) }
 
-  def write_digest(
+  def store(
     database: Option[SQL.Database],
     heap: Path,
     slice: Long,