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