# 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 =