# HG changeset patch
# User wenzelm
# Date 1491823164 -7200
# Node ID ff09d29498b0922b7d56486c9304bf6a5d9ebe1d
# Parent  2b22b7d8649fad1aedab6ce403522ceab30d0d62
proper qualifier for imports;

diff -r 2b22b7d8649f -r ff09d29498b0 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon Apr 10 11:52:21 2017 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon Apr 10 13:19:24 2017 +0200
@@ -312,11 +312,13 @@
                 ("The error(s) above occurred for theory " ^ quote theory_name ^
                   Position.here require_pos ^ required_by "\n" initiators);
 
-          val parents = map (Thy_Header.import_name o #1) imports;
+          val qualifier' = Resources.theory_qualifier theory_name;
+          val dir' = Path.append dir (master_dir_deps (Option.map #1 deps));
+
+          val parents = map (#theory_name o Resources.import_name qualifier' dir' o #1) imports;
           val (parents_current, tasks') =
             require_thys document symbols last_timing (theory_name :: initiators)
-              (Resources.theory_qualifier theory_name)
-              (Path.append dir (master_dir_deps (Option.map #1 deps))) imports tasks;
+              qualifier' dir' imports tasks;
 
           val all_current = current andalso parents_current;
           val task =