clarified signature: ensure disjoint data spaces;

--- a/src/Pure/General/sql.scala	Fri Jul 07 14:17:53 2023 +0200
+++ b/src/Pure/General/sql.scala	Fri Jul 07 14:20:58 2023 +0200
@@ -252,11 +252,10 @@
 
     def transaction_lock[A](
       db: Database,
-      more_tables: Tables = Tables.empty,
       create: Boolean = false,
       synchronized: Boolean = false,
     )(body: => A): A = {
-      def run: A = db.transaction { (tables ::: more_tables).lock(db, create = create); body }
+      def run: A = db.transaction { tables.lock(db, create = create); body }
       if (synchronized) db.synchronized { run } else run
     }
 

--- a/src/Pure/Tools/build_process.scala	Fri Jul 07 14:17:53 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Fri Jul 07 14:20:58 2023 +0200
@@ -845,12 +845,12 @@
   private val _build_database: Option[SQL.Database] =
     try {
       for (db <- store.maybe_open_build_database()) yield {
-        val more_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty
+        val store_tables = if (db.is_postgresql) Store.Data.tables else SQL.Tables.empty
         Build_Process.Data.transaction_lock(db, create = true) {
           Build_Process.Data.clean_build(db)
-          more_tables.lock(db, create = true)
+          store_tables.lock(db, create = true)
         }
-        db.vacuum(Build_Process.Data.tables ::: more_tables)
+        db.vacuum(Build_Process.Data.tables ::: store_tables)
         db
       }
     }