--- a/src/Pure/Thy/export.scala Thu Nov 04 12:37:45 2021 +0100
+++ b/src/Pure/Thy/export.scala Thu Nov 04 12:43:34 2021 +0100
@@ -268,11 +268,11 @@
def database_context(
context: Sessions.Database_Context,
- sessions: List[String],
+ session_hierarchy: List[String],
theory_name: String): Provider =
new Provider {
def apply(export_name: String): Option[Entry] =
- context.read_export(sessions, theory_name, export_name)
+ context.read_export(session_hierarchy, theory_name, export_name)
def focus(other_theory: String): Provider = this