tuned signature;

--- 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,

--- a/src/Pure/Tools/build_job.scala	Wed Jun 21 15:41:18 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Wed Jun 21 15:53:38 2023 +0200
@@ -455,7 +455,7 @@
             val database = store.maybe_open_heaps_database()
             val slice = Space.MiB(options.real("build_database_slice")).bytes
             val digest =
-              try { ML_Heap.write_digest(database, heap, slice = slice) }
+              try { ML_Heap.store(database, heap, slice = slice) }
               finally { database.foreach(_.close()) }
             SHA1.shasum(digest, session_name)
           }