# HG changeset patch
# User wenzelm
# Date 1492765147 -7200
# Node ID d15d302da7f03f1a6f01436f498139a899648e36
# Parent  0d8a7013bf362c3ada896653db57fb0cc3f31cb6
proper theory_qualifier;

diff -r 0d8a7013bf36 -r d15d302da7f0 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 20 17:50:31 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 21 10:59:07 2017 +0200
@@ -164,7 +164,7 @@
               val root_theories =
                 info.theories.flatMap({ case (_, thys) =>
                   thys.map({ case (thy, pos) =>
-                    (resources.import_name(info.name, info.dir.implode, thy), pos) })
+                    (resources.import_name(info.theory_qualifier, info.dir.implode, thy), pos) })
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
@@ -210,10 +210,10 @@
 
               def node(name: Document.Node.Name): Graph_Display.Node =
               {
-                val session = resources.theory_qualifier(name)
-                if (session == info.name)
+                val qualifier = resources.theory_qualifier(name)
+                if (qualifier == info.theory_qualifier)
                   Graph_Display.Node(name.theory_base_name, "theory." + name.theory)
-                else session_node(session)
+                else session_node(qualifier)
               }
 
               val imports_subgraph =