src/Pure/Thy/export.scala
changeset 68205 9a8949f71fd4
parent 68202 a99180ad3441
child 68209 aeffd8f1f079
     1.1 --- a/src/Pure/Thy/export.scala	Thu May 17 15:38:36 2018 +0200
     1.2 +++ b/src/Pure/Thy/export.scala	Thu May 17 16:42:13 2018 +0200
     1.3 @@ -253,13 +253,8 @@
     1.4      /* database */
     1.5  
     1.6      val store = Sessions.store(system_mode)
     1.7 -    val database =
     1.8 -      store.find_database(session_name) match {
     1.9 -        case None => error("Missing database for session " + quote(session_name))
    1.10 -        case Some(database) => database
    1.11 -      }
    1.12  
    1.13 -    using(SQLite.open_database(database))(db =>
    1.14 +    using(SQLite.open_database(store.the_database(session_name)))(db =>
    1.15      {
    1.16        db.transaction {
    1.17          val export_names = read_theory_names(db, session_name)