src/Pure/Thy/export_theory.scala
changeset 68210 65f79c0ddb0d
parent 68209 aeffd8f1f079
child 68222 3c1a716e7f59
--- 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.