# HG changeset patch
# User wenzelm
# Date 1496783633 -7200
# Node ID 96f86c613a9fe46ba10c02e6103ff236f25c49fd
# Parent  77d9334830eceb61c4cc42e22332c5bde652ea04
clarified import of loaded theory;

diff -r 77d9334830ec -r 96f86c613a9f src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Mon Jun 05 21:24:41 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Tue Jun 06 23:13:53 2017 +0200
@@ -141,14 +141,16 @@
           def standard_import(qualifier: String, dir: String, s: String): String =
           {
             val name = imports_resources.import_name(qualifier, dir, s)
-            val file = Path.explode(name.node).file
             val s1 =
-              imports_resources.session_base.known.get_file(file) match {
-                case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
-                  name1.theory
-                case Some(name1) if Thy_Header.is_base_name(s) =>
-                  name1.theory_base_name
-                case _ => s
+              if (session_base.loaded_theory(name)) name.theory
+              else {
+                imports_resources.session_base.known.get_file(Path.explode(name.node).file) match {
+                  case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
+                    name1.theory
+                  case Some(name1) if Thy_Header.is_base_name(s) =>
+                    name1.theory_base_name
+                  case _ => s
+                }
               }
             val name2 = imports_resources.import_name(qualifier, dir, s1)
             if (name.node == name2.node) s1 else s