src/Pure/Thy/sessions.scala

     ): Option[Export.Entry] = {
       val attempts =
         database_server match {
           case Some(db) =>
             sessions.view.map(session_name =>
-              Export.read_entry(db, store.cache, session_name, theory_name, name))
+              Export.Entry_Name(session_name, theory_name, name).read(db, store.cache))
           case None =>
             sessions.view.map(session_name =>
               store.try_open_database(session_name) match {
                 case Some(db) =>
-                  using(db)(Export.read_entry(_, store.cache, session_name, theory_name, name))
+                  using(db)(Export.Entry_Name(session_name, theory_name, name).read(_, store.cache))
                 case None => None
               })
         }
       attempts.collectFirst({ case Some(entry) => entry })
     }