diff -r 7ba63bd216af -r c268def0784b 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) {