# HG changeset patch
# User wenzelm
# Date 1493977089 -7200
# Node ID 3f40afe30feb737f7247ef17852ee846ac8d2d93
# Parent  33368a2296aa85cf2a4189fee21defdfb3ae0616
tuned signature;

diff -r 33368a2296aa -r 3f40afe30feb src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu May 04 22:19:59 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Fri May 05 11:38:09 2017 +0200
@@ -700,7 +700,7 @@
     {
       val recent = recent_table(days)
       val columns1 = if (pull_date) columns ::: List(Data.pull_date(recent)) else columns
-      table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_alias() +
+      table.select(columns1, distinct = distinct) + " INNER JOIN " + recent.query_name +
       " ON " + Prop.isabelle_version(table) + " = " + Prop.isabelle_version(recent)
     }
 
@@ -722,7 +722,7 @@
       val columns = aux_columns ::: sessions_table.columns.tail
       SQL.Table("isabelle_build_log", columns,
         {
-          SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_alias() +
+          SQL.select(log_name(aux_table) :: columns.tail) + aux_table.query_name +
           " INNER JOIN " + table3 + " ON " + log_name(aux_table) + " = " + log_name(table3)
         })
     }
diff -r 33368a2296aa -r 3f40afe30feb src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Thu May 04 22:19:59 2017 +0200
+++ b/src/Pure/General/sql.scala	Fri May 05 11:38:09 2017 +0200
@@ -130,8 +130,7 @@
       if (body == "") error("Missing SQL body for table " + quote(name))
       else SQL.enclose(body)
 
-    def query_alias(alias: String = name): String =
-      query + " AS " + SQL.ident(alias)
+    def query_name: String = query + " AS " + SQL.ident(name)
 
     def create(strict: Boolean = false, sql_type: Type.Value => String): String =
     {