# HG changeset patch
# User wenzelm
# Date 1605369198 -3600
# Node ID b6bce47d0b48fcd5751afa100bea12997fe542ac
# Parent  9576d0faf8f98a0e0c0d92f0d020d297878f26f7
tuned;

diff -r 9576d0faf8f9 -r b6bce47d0b48 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Nov 14 16:49:48 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Nov 14 16:53:18 2020 +0100
@@ -254,20 +254,20 @@
               info.document_theories.flatMap(
               {
                 case (thy, pos) =>
-                  val ancestors = sessions_structure.build_requirements(List(session_name))
+                  val parent_sessions = sessions_structure.build_requirements(List(session_name))
 
                   def err(msg: String): Option[String] =
                     Some(msg + " " + quote(thy) + Position.here(pos))
 
-                  known_theories.get(thy) match {
+                  known_theories.get(thy).map(_.name) match {
                     case None => err("Unknown document theory")
-                    case Some(entry) =>
-                      val qualifier = deps_base.theory_qualifier(entry.name)
-                      if (session_theories.contains(entry.name)) {
+                    case Some(name) =>
+                      val qualifier = deps_base.theory_qualifier(name)
+                      if (session_theories.contains(name)) {
                         err("Redundant document theory from this session:")
                       }
-                      else if (ancestors.contains(qualifier)) None
-                      else if (dependencies.theories.contains(entry.name)) None
+                      else if (parent_sessions.contains(qualifier)) None
+                      else if (dependencies.theories.contains(name)) None
                       else err("Document theory from other session not imported properly:")
                   }
               })