diff -r 8dc9d979bbac -r b6d74c90b588 src/Pure/Thy/document_build.scala --- a/src/Pure/Thy/document_build.scala Wed Aug 03 13:07:32 2022 +0200 +++ b/src/Pure/Thy/document_build.scala Wed Aug 03 13:49:41 2022 +0200 @@ -167,8 +167,10 @@ def documents: List[Document_Variant] = info.documents - def session_theories: List[Document.Node.Name] = base.session_theories - def document_theories: List[Document.Node.Name] = session_theories ::: base.document_theories + def proper_session_theories: List[Document.Node.Name] = base.proper_session_theories + + def document_theories: List[Document.Node.Name] = + proper_session_theories ::: base.document_theories lazy val document_latex: List[File.Content_XML] = for (name <- document_theories) @@ -188,7 +190,7 @@ val path = Path.basic("session.tex") val content = Library.terminate_lines( - base.session_theories.map(name => "\\input{" + tex_name(name) + "}")) + base.proper_session_theories.map(name => "\\input{" + tex_name(name) + "}")) File.Content(path, content) }