# HG changeset patch
# User wenzelm
# Date 1492785932 -7200
# Node ID 23c2450ae02756c27f5528f2a6f7e78a0c2d4d84
# Parent  1bf7b5dc34c88342da59dab0033c62a84f83055a
clarified: explicit check of result;

diff -r 1bf7b5dc34c8 -r 23c2450ae027 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 =