# HG changeset patch
# User wenzelm
# Date 1605368988 -3600
# Node ID 9576d0faf8f98a0e0c0d92f0d020d297878f26f7
# Parent  b040c9e672856331d19a730263437eed892c3f87
proper theory name;

diff -r b040c9e67285 -r 9576d0faf8f9 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Nov 14 13:01:12 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Sat Nov 14 16:49:48 2020 +0100
@@ -255,7 +255,6 @@
               {
                 case (thy, pos) =>
                   val ancestors = sessions_structure.build_requirements(List(session_name))
-                  val qualifier = deps_base.theory_qualifier(session_name)
 
                   def err(msg: String): Option[String] =
                     Some(msg + " " + quote(thy) + Position.here(pos))
@@ -263,6 +262,7 @@
                   known_theories.get(thy) match {
                     case None => err("Unknown document theory")
                     case Some(entry) =>
+                      val qualifier = deps_base.theory_qualifier(entry.name)
                       if (session_theories.contains(entry.name)) {
                         err("Redundant document theory from this session:")
                       }