# HG changeset patch
# User wenzelm
# Date 1660494959 -7200
# Node ID 186654cd2840bf7052bf8205f690bdcb21df9fea
# Parent  c32ecc4b4720ae38bfa4e270ee0be6f515564473
clarified signature;

diff -r c32ecc4b4720 -r 186654cd2840 src/Pure/Thy/export_theory.scala
--- a/src/Pure/Thy/export_theory.scala	Sun Aug 14 12:18:06 2022 +0200
+++ b/src/Pure/Thy/export_theory.scala	Sun Aug 14 18:35:59 2022 +0200
@@ -26,10 +26,11 @@
 
   def read_session(
     session_context: Export.Session_Context,
+    session_stack: Boolean = false,
     progress: Progress = new Progress
   ): Session = {
     val thys =
-      for (theory <- theory_names(session_context)) yield {
+      for (theory <- theory_names(session_context, session_stack = session_stack)) yield {
         progress.echo("Reading theory " + theory)
         read_theory(session_context.theory(theory))
       }
@@ -104,11 +105,16 @@
     theory_context.get(Export.THEORY_PREFIX + "parents")
       .map(entry => Library.trim_split_lines(entry.uncompressed.text))
 
-  def theory_names(session_context: Export.Session_Context): List[String] =
+  def theory_names(
+    session_context: Export.Session_Context,
+    session_stack: Boolean = false
+  ): List[String] = {
+    val session = if (session_stack) "" else session_context.session_name
     for {
-      theory <- session_context.theory_names()
+      theory <- session_context.theory_names(session = session)
       if read_theory_parents(session_context.theory(theory)).isDefined
     } yield theory
+  }
 
   def no_theory: Theory =
     Theory("", Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Nil, Map.empty)