diff -r 03eb7f7bb990 -r d8c99a497502 src/Pure/General/sql.scala --- 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")