tuned signature;

--- a/src/Pure/Thy/export.scala	Fri May 18 17:09:55 2018 +0200
+++ b/src/Pure/Thy/export.scala	Fri May 18 17:21:12 2018 +0200
@@ -254,7 +254,7 @@
 
     val store = Sessions.store(options, system_mode)
 
-    using(SQLite.open_database(store.the_database(session_name)))(db =>
+    using(store.open_database(session_name))(db =>
     {
       db.transaction {
         val export_names = read_theory_names(db, session_name)

--- a/src/Pure/Thy/export_theory.scala	Fri May 18 17:09:55 2018 +0200
+++ b/src/Pure/Thy/export_theory.scala	Fri May 18 17:21:12 2018 +0200
@@ -29,7 +29,7 @@
     consts: Boolean = true): Session =
   {
     val thys =
-      using(SQLite.open_database(store.the_database(session_name)))(db =>
+      using(store.open_database(session_name))(db =>
       {
         db.transaction {
           Export.read_theory_names(db, session_name).iterator.map(_._1).toSet.iterator.

--- a/src/Pure/Thy/sessions.scala	Fri May 18 17:09:55 2018 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri May 18 17:21:12 2018 +0200
@@ -1026,8 +1026,9 @@
     def find_database(name: String): Option[Path] =
       input_dirs.map(_ + database(name)).find(_.is_file)
 
-    def the_database(name: String): Path =
-      find_database(name) getOrElse error("Missing database for session " + quote(name))
+    def open_database(name: String): SQL.Database =
+      SQLite.open_database(
+        find_database(name) getOrElse error("Missing database for session " + quote(name)))
 
     def heap(name: String): Path =
       input_dirs.map(_ + Path.basic(name)).find(_.is_file) getOrElse