proper qualifier for imports;
authorwenzelm
Mon, 10 Apr 2017 13:19:24 +0200
changeset 65455 ff09d29498b0
parent 65454 2b22b7d8649f
child 65456 31e8a86971a8
proper qualifier for imports;
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 =