# HG changeset patch
# User wenzelm
# Date 1710185495 -3600
# Node ID bc979e334c7dfe6726e07f8b444c98dbdd1bffec
# Parent  ee4864e17c1173bb2a6cff240fa0d296f2448151
tuned signature;

diff -r ee4864e17c11 -r bc979e334c7d src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Mon Mar 11 20:24:59 2024 +0100
+++ b/src/Pure/Admin/build_log.scala	Mon Mar 11 20:31:35 2024 +0100
@@ -1278,7 +1278,7 @@
 
           val columns =
             table1.columns.map(c => c(table1)) :::
-              List(Column.known.copy(expr = Column.log_name(aux_table).defined))
+              List(Column.known.make_expr(Column.log_name(aux_table).defined))
 
           SQL.select(columns, distinct = true) +
             table1.query_named + SQL.join_outer + aux_table.query_named +
diff -r ee4864e17c11 -r bc979e334c7d src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Mon Mar 11 20:24:59 2024 +0100
+++ b/src/Pure/General/sql.scala	Mon Mar 11 20:31:35 2024 +0100
@@ -173,7 +173,8 @@
     def where_member_long(set: Iterable[Long]): Source = SQL.where(member_long(set))
     def where_member(set: Iterable[String]): Source = SQL.where(member(set))
 
-    def max: Column = copy(expr = "MAX(" + ident + ")")
+    def make_expr(e: SQL.Source): Column = copy(expr = e)
+    def max: Column = make_expr("MAX(" + ident + ")")
 
     override def toString: Source = ident
   }