clarified signature;

--- a/src/Pure/Admin/build_log.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -658,21 +658,23 @@
     val known = SQL.Column.bool("known")
 
     val meta_info_table =
-      make_table("meta_info", log_name :: Prop.all_props ::: Settings.all_settings)
+      make_table(log_name :: Prop.all_props ::: Settings.all_settings, name = "meta_info")
 
     val sessions_table =
-      make_table("sessions",
+      make_table(
         List(log_name, session_name, chapter, groups, threads, timing_elapsed, timing_cpu,
           timing_gc, timing_factor, ml_timing_elapsed, ml_timing_cpu, ml_timing_gc, ml_timing_factor,
-          heap_size, status, errors, sources))
+          heap_size, status, errors, sources),
+        name = "sessions")
 
     val theories_table =
-      make_table("theories",
+      make_table(
         List(log_name, session_name, theory_name, theory_timing_elapsed, theory_timing_cpu,
-          theory_timing_gc))
+          theory_timing_gc),
+        name = "theories")
 
     val ml_statistics_table =
-      make_table("ml_statistics", List(log_name, session_name, ml_statistics))
+      make_table(List(log_name, session_name, ml_statistics), name = "ml_statistics")
 
 
     /* AFP versions */
@@ -680,9 +682,11 @@
     val isabelle_afp_versions_table: SQL.Table = {
       val version1 = Prop.isabelle_version
       val version2 = Prop.afp_version
-      make_table("isabelle_afp_versions", List(version1.make_primary_key, version2),
-        SQL.select(List(version1, version2), distinct = true) + meta_info_table +
-          SQL.where_and(version1.defined, version2.defined))
+      make_table(List(version1.make_primary_key, version2),
+        body =
+          SQL.select(List(version1, version2), distinct = true) + meta_info_table +
+            SQL.where_and(version1.defined, version2.defined),
+        name = "isabelle_afp_versions")
     }
 
 
@@ -697,12 +701,14 @@
         if (afp) ("afp_pull_date", List(Prop.isabelle_version, Prop.afp_version))
         else ("pull_date", List(Prop.isabelle_version))
 
-      make_table(name, versions.map(_.make_primary_key) ::: List(pull_date(afp)),
-        "SELECT " + versions.mkString(", ") +
-          ", min(" + Prop.build_start + ") AS " + pull_date(afp) +
-        " FROM " + meta_info_table +
-        " WHERE " + SQL.AND((versions ::: List(Prop.build_start)).map(_.defined)) +
-        " GROUP BY " + versions.mkString(", "))
+      make_table(versions.map(_.make_primary_key) ::: List(pull_date(afp)),
+        body =
+          "SELECT " + versions.mkString(", ") +
+            ", min(" + Prop.build_start + ") AS " + pull_date(afp) +
+          " FROM " + meta_info_table +
+          " WHERE " + SQL.AND((versions ::: List(Prop.build_start)).map(_.defined)) +
+          " GROUP BY " + versions.mkString(", "),
+        name = name)
     }
 
 
@@ -794,14 +800,13 @@
           b_table.query_named + SQL.join_inner + sessions_table +
           " ON " + log_name(b_table) + " = " + log_name(sessions_table))
 
-      make_table("", c_columns ::: List(ml_statistics),
-        {
+      make_table(c_columns ::: List(ml_statistics),
+        body =
           SQL.select(c_columns.map(_.apply(c_table)) ::: List(ml_statistics)) +
           c_table.query_named + SQL.join_outer + ml_statistics_table + " ON " +
             SQL.and(
               log_name(c_table).ident + " = " + log_name(ml_statistics_table).ident,
-              session_name(c_table).ident + " = " + session_name(ml_statistics_table).ident)
-        })
+              session_name(c_table).ident + " = " + session_name(ml_statistics_table).ident))
     }
   }
 

--- a/src/Pure/General/sql.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/General/sql.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -259,7 +259,7 @@
       if (synchronized) db.synchronized { run } else run
     }
 
-    def make_table(name: String, columns: List[Column], body: String = ""): Table = {
+    def make_table(columns: List[Column], body: String = "", name: String = ""): Table = {
       val table_name =
         List(proper_string(table_prefix), proper_string(name)).flatten.mkString("_")
       require(table_name.nonEmpty, "Undefined database table name")

--- a/src/Pure/ML/ml_heap.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/ML/ml_heap.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -55,7 +55,7 @@
       val size = SQL.Column.long("size")
       val digest = SQL.Column.string("digest")
 
-      val table = make_table("", List(name, size, digest))
+      val table = make_table(List(name, size, digest))
     }
 
     object Slices {
@@ -63,7 +63,7 @@
       val slice = SQL.Column.int("slice").make_primary_key
       val content = SQL.Column.bytes("content")
 
-      val table = make_table("slices", List(name, slice, content))
+      val table = make_table(List(name, slice, content), name = "slices")
     }
 
     def get_entry(db: SQL.Database, name: String): Option[SHA1.Digest] =

--- a/src/Pure/System/host.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/System/host.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -104,7 +104,7 @@
       val hostname = SQL.Column.string("hostname").make_primary_key
       val numa_next = SQL.Column.int("numa_next")
 
-      val table = make_table("node_info", List(hostname, numa_next))
+      val table = make_table(List(hostname, numa_next), name = "node_info")
     }
 
     def read_numa_next(db: SQL.Database, hostname: String): Int =

--- a/src/Pure/System/progress.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/System/progress.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -51,7 +51,7 @@
       val context = SQL.Column.long("context").make_primary_key
       val stopped = SQL.Column.bool("stopped")
 
-      val table = make_table("", List(context_uuid, context, stopped))
+      val table = make_table(List(context_uuid, context, stopped))
     }
 
     object Agents {
@@ -66,8 +66,10 @@
       val stop = SQL.Column.date("stop")
       val seen = SQL.Column.long("seen")
 
-      val table = make_table("agents",
-        List(agent_uuid, context_uuid, kind, hostname, java_pid, java_start, start, stamp, stop, seen))
+      val table =
+        make_table(
+          List(agent_uuid, context_uuid, kind, hostname, java_pid, java_start, start, stamp, stop, seen),
+          name = "agents")
     }
 
     object Messages {
@@ -80,7 +82,7 @@
       val text = SQL.Column.string("text")
       val verbose = SQL.Column.bool("verbose")
 
-      val table = make_table("messages", List(context, serial, kind, text, verbose))
+      val table = make_table(List(context, serial, kind, text, verbose), name = "messages")
     }
 
     def read_progress_context(db: SQL.Database, context_uuid: String): Option[Long] =

--- a/src/Pure/Thy/document_build.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/Thy/document_build.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -64,7 +64,7 @@
       val log_xz = SQL.Column.bytes("log_xz")
       val pdf = SQL.Column.bytes("pdf")
 
-      val table = make_table("", List(session_name, name, sources, log_xz, pdf))
+      val table = make_table(List(session_name, name, sources, log_xz, pdf))
     }
 
     def where_equal(session_name: String, name: String = ""): SQL.Source =

--- a/src/Pure/Tools/build_process.scala	Fri Jul 07 18:04:45 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sat Jul 08 13:13:10 2023 +0200
@@ -342,7 +342,7 @@
       val start = SQL.Column.date("start")
       val stop = SQL.Column.date("stop")
 
-      val table = make_table("", List(build_uuid, ml_platform, options, start, stop))
+      val table = make_table(List(build_uuid, ml_platform, options, start, stop))
     }
 
     def read_builds(db: SQL.Database, build_uuid: String = ""): List[Build] = {
@@ -413,9 +413,11 @@
       val old_command_timings = SQL.Column.bytes("old_command_timings")
       val build_uuid = Generic.build_uuid
 
-      val table = make_table("sessions",
-        List(name, deps, ancestors, options, sources, timeout,
-          old_time, old_command_timings, build_uuid))
+      val table =
+        make_table(
+          List(name, deps, ancestors, options, sources, timeout,
+            old_time, old_command_timings, build_uuid),
+          name = "sessions")
     }
 
     def read_sessions_domain(db: SQL.Database, build_uuid: String = ""): Set[String] =
@@ -485,7 +487,8 @@
       val stop = SQL.Column.date("stop")
       val serial = SQL.Column.long("serial")
 
-      val table = make_table("workers", List(worker_uuid, build_uuid, start, stamp, stop, serial))
+      val table =
+        make_table(List(worker_uuid, build_uuid, start, stamp, stop, serial), name = "workers")
     }
 
     def read_serial(db: SQL.Database): Long =
@@ -575,7 +578,7 @@
       val info = SQL.Column.string("info")
       val build_uuid = Generic.build_uuid
 
-      val table = make_table("pending", List(name, deps, info, build_uuid))
+      val table = make_table(List(name, deps, info, build_uuid), name = "pending")
     }
 
     def read_pending(db: SQL.Database): List[Task] =
@@ -622,7 +625,8 @@
       val hostname = SQL.Column.string("hostname")
       val numa_node = SQL.Column.int("numa_node")
 
-      val table = make_table("running", List(name, worker_uuid, build_uuid, hostname, numa_node))
+      val table =
+        make_table(List(name, worker_uuid, build_uuid, hostname, numa_node), name = "running")
     }
 
     def read_running(db: SQL.Database): State.Running =
@@ -683,9 +687,10 @@
       val current = SQL.Column.bool("current")
 
       val table =
-        make_table("results",
+        make_table(
           List(name, worker_uuid, build_uuid, hostname, numa_node,
-            rc, out, err, timing_elapsed, timing_cpu, timing_gc, output_shasum, current))
+            rc, out, err, timing_elapsed, timing_cpu, timing_gc, output_shasum, current),
+          name = "results")
     }
 
     def read_results_domain(db: SQL.Database): Set[String] =