src/Pure/Thy/store.scala

--- a/src/Pure/Thy/store.scala	Fri Jun 23 13:51:23 2023 +0200
+++ b/src/Pure/Thy/store.scala	Fri Jun 23 14:43:15 2023 +0200
@@ -316,8 +316,8 @@
         path = dir + file if path.is_file
       } yield path.file.delete
 
-    for (db <- maybe_open_heaps_database()) {
-      using(db)(ML_Heap.clean_entry(_, name))
+    using_optional(maybe_open_heaps_database()) { database =>
+      database.foreach(ML_Heap.clean_entry(_, name))
     }
 
     if (init) {