# HG changeset patch
# User wenzelm
# Date 1636026214 -3600
# Node ID 42f358ea8deed876a85711ec1ac2df4c991182a3
# Parent  0ab5e35ac964ef4fef8cb691e20847b49c78aa87
tuned;

diff -r 0ab5e35ac964 -r 42f358ea8dee src/Pure/Thy/export.scala
--- 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