# HG changeset patch
# User wenzelm
# Date 1492677300 -7200
# Node ID f47bc12b6e8a2ea1391fc04efdf41c5b731de5eb
# Parent  d244d8f8e13fc8b0c9b8accb0e90f211ed45cabc
clarified;

diff -r d244d8f8e13f -r f47bc12b6e8a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Apr 20 10:30:30 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Apr 20 10:35:00 2017 +0200
@@ -150,8 +150,7 @@
               parent_base.copy(known =
                 Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
 
-            val resources = new Resources(imports_base,
-              default_qualifier = info.theory_qualifier(info.name))
+            val resources = new Resources(imports_base, default_qualifier = info.theory_qualifier)
 
             if (verbose || list_files) {
               val groups =
@@ -301,9 +300,9 @@
   {
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
-    def theory_qualifier(default_qualifier: String): String =
+    def theory_qualifier: String =
       options.string("theory_qualifier") match {
-        case "" => default_qualifier
+        case "" => name
         case qualifier => qualifier
       }
   }
@@ -421,7 +420,7 @@
           thy <- info.global_theories.iterator }
          yield (thy, info)))({
             case (global, (thy, info)) =>
-              val qualifier = info.theory_qualifier(info.name)
+              val qualifier = info.theory_qualifier
               global.get(thy) match {
                 case Some(qualifier1) if qualifier != qualifier1 =>
                   error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
diff -r d244d8f8e13f -r f47bc12b6e8a src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Thu Apr 20 10:30:30 2017 +0200
+++ b/src/Pure/Tools/build.scala	Thu Apr 20 10:35:00 2017 +0200
@@ -223,8 +223,7 @@
             ML_Syntax.print_string0(File.platform_path(output))
 
         if (pide && !Sessions.is_pure(name)) {
-          val resources =
-            new Resources(deps(parent), default_qualifier = info.theory_qualifier(name))
+          val resources = new Resources(deps(parent), default_qualifier = info.theory_qualifier)
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)