# HG changeset patch
# User wenzelm
# Date 1637151118 -3600
# Node ID 4543fb2b5ef24bdda546f56caa2f9dbd68d4048e
# Parent  1f40ded31b78dae238f1138ddceefa64c17eeee6
tuned;

diff -r 1f40ded31b78 -r 4543fb2b5ef2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Nov 17 12:55:02 2021 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Nov 17 13:11:58 2021 +0100
@@ -267,9 +267,9 @@
               info.document_theories.flatMap(
               {
                 case (thy, pos) =>
-                  val parent_sessions =
+                  val build_hierarchy =
                     if (sessions_structure.build_graph.defined(session_name)) {
-                      sessions_structure.build_requirements(List(session_name))
+                      sessions_structure.build_hierarchy(session_name)
                     }
                     else Nil
 
@@ -283,7 +283,7 @@
                       if (session_theories.contains(name)) {
                         err("Redundant document theory from this session:")
                       }
-                      else if (parent_sessions.contains(qualifier)) None
+                      else if (build_hierarchy.contains(qualifier)) None
                       else if (dependencies.theories.contains(name)) None
                       else err("Document theory from other session not imported properly:")
                   }