src/Pure/Tools/imports.scala
changeset 66767 294c2e9a689e
parent 66737 2edc0c42c883
child 66780 bf54ca580bf2
     1.1 --- a/src/Pure/Tools/imports.scala	Thu Oct 05 14:58:04 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Thu Oct 05 16:33:36 2017 +0200
     1.3 @@ -141,22 +141,7 @@
     1.4            val imports_resources = new Resources(imports_base)
     1.5  
     1.6            def standard_import(qualifier: String, dir: String, s: String): String =
     1.7 -          {
     1.8 -            val name = imports_resources.import_name(qualifier, dir, s)
     1.9 -            val s1 =
    1.10 -              if (imports_base.loaded_theory(name)) name.theory
    1.11 -              else {
    1.12 -                imports_base.known.get_file(name.path.file) match {
    1.13 -                  case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
    1.14 -                    name1.theory
    1.15 -                  case Some(name1) if Thy_Header.is_base_name(s) =>
    1.16 -                    name1.theory_base_name
    1.17 -                  case _ => s
    1.18 -                }
    1.19 -              }
    1.20 -            val name2 = imports_resources.import_name(qualifier, dir, s1)
    1.21 -            if (name.node == name2.node) s1 else s
    1.22 -          }
    1.23 +            imports_resources.standard_import(session_resources, qualifier, dir, s)
    1.24  
    1.25            val updates_root =
    1.26              for {