diff -r f2e402a19530 -r ca8ae1ffd2b8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Jul 11 08:21:54 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Jul 11 13:21:22 2022 +0200
@@ -1216,12 +1216,12 @@
         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
               })
         }