# HG changeset patch # User wenzelm # Date 1489926979 -3600 # Node ID b2dc9e3b8ee5b38bd54ee74c7b7726f4162e9f50 # Parent 2b1cd063e0b25d0d1e071f0e385f319a424aa305 tuned; diff -r 2b1cd063e0b2 -r b2dc9e3b8ee5 src/Pure/Thy/sessions.scala --- a/src/Pure/Thy/sessions.scala Sun Mar 19 13:34:47 2017 +0100 +++ b/src/Pure/Thy/sessions.scala Sun Mar 19 13:36:19 2017 +0100 @@ -537,7 +537,7 @@ val table = SQL.Table("isabelle_session_info", build_log_columns ::: build_columns) def where_session_name(name: String): String = - "WHERE " + SQL.quote_ident(session_name.name) + " = " + SQL.quote_string(name) + "WHERE " + session_name.sql_name + " = " + SQL.quote_string(name) def select_statement(db: SQL.Database, name: String, columns: List[SQL.Column]) : PreparedStatement =