src/Pure/Thy/export.scala

     Entry(session_name, args.theory_name, args.name,
       if (args.compress) Future.fork(body.maybe_compress(cache = cache))
       else Future.value((false, body)))
   }
 
-  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String): Entry =
+  def read_entry(db: SQL.Database, session_name: String, theory_name: String, name: String)
+    : Option[Entry] =
   {
     val select =
       Data.table.select(List(Data.compressed, Data.body),
         Data.where_equal(session_name, theory_name, name))
     db.using_statement(select)(stmt =>
     {
       val res = stmt.execute_query()
       if (res.next()) {
         val compressed = res.bool(Data.compressed)
         val body = res.bytes(Data.body)
-        Entry(session_name, theory_name, name, Future.value(compressed, body))
-      }
-      else error(message("Bad export", theory_name, name))
+        Some(Entry(session_name, theory_name, name, Future.value(compressed, body)))
+      }
+      else None
     })
   }
 
 
   /* database consumer thread */

         // export
         if (export_pattern != "") {
           val xz_cache = XZ.make_cache()
 
           val matcher = make_matcher(export_pattern)
-          for { (theory_name, name) <- export_names if matcher(theory_name, name) }
-          {
-            val entry = read_entry(db, session_name, theory_name, name)
+          for {
+            (theory_name, name) <- export_names if matcher(theory_name, name)
+            entry <- read_entry(db, session_name, theory_name, name)
+          } {
             val path = export_dir + Path.basic(theory_name) + Path.explode(name)
-
             progress.echo("exporting " + path)
             Isabelle_System.mkdirs(path.dir)
             Bytes.write(path, entry.uncompressed(cache = xz_cache))
           }
         }