# HG changeset patch
# User wenzelm
# Date 1493904057 -7200
# Node ID 01fc771021e67b64f283c0fc75da3e9791bf51c1
# Parent  79be5b464a1642389b539e3b6dad5d28ef126eea
redundant;

diff -r 79be5b464a16 -r 01fc771021e6 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Thu May 04 15:10:51 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Thu May 04 15:20:57 2017 +0200
@@ -678,9 +678,7 @@
     // WARNING: This may cause performance problems, e.g. with sqlitebrowser
     val full_table: SQL.Table =
     {
-      val columns =
-        meta_info_table.columns :::
-          sessions_table.columns.tail.map(_.copy(primary_key = false))
+      val columns = meta_info_table.columns ::: sessions_table.columns.tail
       SQL.Table("isabelle_build_log", columns,
         {
           val table1 = meta_info_table