tuned;

--- a/src/Pure/Admin/build_history.scala	Thu Jun 15 15:04:23 2023 +0200
+++ b/src/Pure/Admin/build_history.scala	Thu Jun 15 17:03:48 2023 +0200
@@ -314,8 +314,7 @@
 
           val properties =
             if (database.is_file) {
-              using(SQLite.open_database(database))(db =>
-                store.read_ml_statistics(db, session_name))
+              using(SQLite.open_database(database))(store.read_ml_statistics(_, session_name))
             }
             else if (log_gz.is_file) {
               Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics
@@ -340,7 +339,7 @@
           val errors =
             if (database.is_file) {
               try {
-                using(SQLite.open_database(database))(db => store.read_errors(db, session_name))
+                using(SQLite.open_database(database))(store.read_errors(_, session_name))
               } // column "errors" could be missing
               catch { case _: java.sql.SQLException => Nil }
             }

--- a/src/Pure/Tools/server.scala	Thu Jun 15 15:04:23 2023 +0200
+++ b/src/Pure/Tools/server.scala	Thu Jun 15 17:03:48 2023 +0200
@@ -429,7 +429,7 @@
   }
 
   def exit(name: String = default_name): Boolean = {
-    using(SQLite.open_database(Data.database))(db =>
+    using(SQLite.open_database(Data.database)) { db =>
       db.transaction_lock(Data.tables) {
         find(db, name) match {
           case Some(server_info) =>
@@ -438,7 +438,8 @@
             true
           case None => false
         }
-      })
+      }
+    }
   }