src/Pure/Thy/export.scala

     val select = Data.table.select(List(Data.name), Data.where_equal(session_name, theory_name))
     db.using_statement(select)(stmt =>
       stmt.execute_query().iterator(res => res.string(Data.name)).toList)
   }
 
+  def message(msg: String, theory_name: String, name: String): String =
+    msg + " " + quote(name) + " for theory " + quote(theory_name)
+
   sealed case class Entry(
     session_name: String,
     theory_name: String,
     name: String,
     compressed: Boolean,
     body: Future[Bytes])
   {
     override def toString: String = theory_name + ":" + name
-
-    def message(msg: String): String =
-      msg + " " + quote(name) + " for theory " + quote(theory_name)
 
     def write(db: SQL.Database)
     {
       val bytes = body.join
       db.using_statement(Data.table.insert())(stmt =>

       if (res.next()) {
         val compressed = res.bool(Data.compressed)
         val body = res.bytes(Data.body)
         Entry(session_name, theory_name, name, compressed, Future.value(body))
       }
-      else error(Entry(session_name, theory_name, name, false, Future.value(Bytes.empty)).message("Bad export"))
+      else error(message("Bad export", theory_name, name))
     })
   }
 
 
   /* database consumer thread */

       Consumer_Thread.fork(name = "export")(consume = (entry: Entry) =>
         {
           entry.body.join
           db.transaction {
             if (read_names(db, entry.session_name, entry.theory_name).contains(entry.name)) {
-              export_errors.change(errs => entry.message("Duplicate export") :: errs)
+              val err = message("Duplicate export", entry.theory_name, entry.name)
+              export_errors.change(errs => err :: errs)
             }
             else entry.write(db)
           }
           true
         })