src/Pure/Thy/export_theory.scala

     progress: Progress = new Progress,
     cache: Term.Cache = Term.Cache.make()): Session = {
     val thys =
       sessions_structure.build_requirements(List(session_name)).flatMap(session =>
         using(store.open_database(session)) { db =>
-          db.transaction {
-            for (theory <- Export.read_theory_names(db, session))
-            yield {
-              progress.echo("Reading theory " + theory)
-              val provider = Export.Provider.database(db, store.cache, session, theory)
-              read_theory(provider, session, theory, cache = cache)
-            }
+          for (theory <- Export.read_theory_names(db, session))
+          yield {
+            progress.echo("Reading theory " + theory)
+            val provider = Export.Provider.database(db, store.cache, session, theory)
+            read_theory(provider, session, theory, cache = cache)
           }
         })
 
     val graph0 =
       thys.foldLeft(Graph.string[Option[Theory]]) {

   def read_pure[A](store: Sessions.Store, read: (Export.Provider, String, String) => A): A = {
     val session_name = Thy_Header.PURE
     val theory_name = Thy_Header.PURE
 
     using(store.open_database(session_name)) { db =>
-      db.transaction {
-        val provider = Export.Provider.database(db, store.cache, session_name, theory_name)
-        read(provider, session_name, theory_name)
-      }
+      val provider = Export.Provider.database(db, store.cache, session_name, theory_name)
+      read(provider, session_name, theory_name)
     }
   }
 
   def read_pure_theory(store: Sessions.Store, cache: Term.Cache = Term.Cache.none): Theory =
     read_pure(store, read_theory(_, _, _, cache = cache))