# HG changeset patch
# User wenzelm
# Date 1670848098 -3600
# Node ID 2542ea38221545f3575fd6be491f8e97f1440748
# Parent  117cb1c35564bf00434a35a5ad9c4ff0af34eaee
tuned;

diff -r 117cb1c35564 -r 2542ea382215 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sun Dec 11 20:27:40 2022 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Dec 12 13:28:18 2022 +0100
@@ -379,9 +379,13 @@
                       if (proper_session_theories.contains(name)) {
                         err("Redundant document theory from this session:")
                       }
-                      else if (build_hierarchy.contains(qualifier)) None
-                      else if (dependencies.theories.contains(name)) None
-                      else err("Document theory from other session not imported properly:")
+                      else if (
+                        !build_hierarchy.contains(qualifier) &&
+                        !dependencies.theories.contains(name)
+                      ) {
+                        err("Document theory from other session not imported properly:")
+                      }
+                      else None
                   }
               })
             val document_theories =