src/Pure/Thy/sessions.scala

--- a/src/Pure/Thy/sessions.scala	Tue Jul 12 15:42:57 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Jul 12 16:04:15 2022 +0200
@@ -1259,7 +1259,7 @@
               for {
                 entry_name <- Export.read_entry_names(db, name) if matcher(entry_name)
                 entry <- entry_name.read(db, store.cache)
-              } yield File.Content(Path.make(entry.entry_name.elements()), entry.uncompressed)
+              } yield File.Content(entry.entry_name.make_path(), entry.uncompressed)
             Some(res)
           }
         ).getOrElse(Nil)