proper theory name;
authorwenzelm
Sat, 14 Nov 2020 16:49:48 +0100
changeset 72839 9576d0faf8f9
parent 72838 b040c9e67285
child 72840 b6bce47d0b48
proper theory name;
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:")
                       }