clarified: explicit check of result;
authorwenzelm
Fri, 21 Apr 2017 16:45:32 +0200
changeset 65536 23c2450ae027
parent 65535 1bf7b5dc34c8
child 65537 7ce5fcebfb35
clarified: explicit check of result;
src/Pure/Tools/update_imports.scala
--- a/src/Pure/Tools/update_imports.scala	Fri Apr 21 16:12:11 2017 +0200
+++ b/src/Pure/Tools/update_imports.scala	Fri Apr 21 16:45:32 2017 +0200
@@ -78,10 +78,13 @@
       def standard_import(qualifier: String, dir: String, s: String): String =
       {
         val name = resources.import_name(qualifier, dir, s)
-        if (!local_theories.contains(name)) s
-        if (resources.theory_qualifier(name) != qualifier) name.theory
-        else if (Thy_Header.is_base_name(s)) name.theory_base_name
-        else s
+        val s1 =
+          if (!local_theories.contains(name)) s
+          else if (resources.theory_qualifier(name) != qualifier) name.theory
+          else if (Thy_Header.is_base_name(s)) name.theory_base_name
+          else s
+        val name1 = resources.import_name(qualifier, dir, s1)
+        if (name == name1) s1 else s
       }
 
       val updates_root =