src/Pure/Thy/thy_info.ML

     val _ = Output.urgent_message ("Loading theory " ^ quote name ^ required_by " " initiators);
 
     val {master = (thy_path, _), imports} = deps;
     val dir = Path.dir thy_path;
     val pos = Path.position thy_path;
-    val uses = map (apfst Path.explode) (#3 (Thy_Header.read pos text));
+    val (_, _, uses) = Thy_Header.read pos text;
     fun init _ =
       Thy_Load.begin_theory dir name imports parent_thys uses
       |> Present.begin_theory update_time dir uses;
 
     val (after_load, theory) = Outer_Syntax.load_thy name init pos text;

 
   in (theory, after_load') end;
 
 fun check_deps dir name =
   (case lookup_deps name of
-    SOME NONE => (true, NONE, get_parents name, NONE)
+    SOME NONE => (true, NONE, get_parents name)
   | NONE =>
-      let val {master, text, imports, ...} = Thy_Load.deps_thy dir name
-      in (false, SOME (make_deps master imports), imports, SOME text) end
+      let val {master, text, imports, ...} = Thy_Load.check_thy dir name
+      in (false, SOME (make_deps master imports, text), imports) end
   | SOME (SOME {master, imports}) =>
-      let val master' = Thy_Load.check_thy dir name in
-        if #2 master <> #2 master' then
-          let val {text = text', imports = imports', ...} = Thy_Load.deps_thy dir name;
-          in (false, SOME (make_deps master' imports'), imports', SOME text') end
-        else
-          let
-            val current =
-              (case lookup_theory name of
-                NONE => false
-              | SOME theory => Thy_Load.all_current theory);
-            val deps' = SOME (make_deps master' imports);
-          in (current, deps', imports, NONE) end
-      end);
+      let
+        val {master = master', text = text', imports = imports', ...} = Thy_Load.check_thy dir name;
+        val deps' = SOME (make_deps master' imports', text');
+        val current =
+          #2 master = #2 master' andalso
+            (case lookup_theory name of
+              NONE => false
+            | SOME theory => Thy_Load.all_current theory);
+      in (current, deps', imports') end);
 
 in
 
 fun require_thys initiators dir strs tasks =
       fold_map (require_thy initiators dir) strs tasks |>> forall I

   in
     (case try (Graph.get_node tasks) name of
       SOME task => (task_finished task, tasks)
     | NONE =>
         let
-          val (current, deps, imports, opt_text) = check_deps dir' name
+          val (current, deps, imports) = check_deps dir' name
             handle ERROR msg => cat_error msg
               (loader_msg "the error(s) above occurred while examining theory" [name] ^
                 required_by "\n" initiators);
 
           val parents = map base_name imports;
           val (parents_current, tasks') =
-            require_thys (name :: initiators) (Path.append dir (master_dir deps)) imports tasks;
+            require_thys (name :: initiators)
+              (Path.append dir (master_dir (Option.map #1 deps))) imports tasks;
 
           val all_current = current andalso parents_current;
           val task =
             if all_current then Finished (get_theory name)
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
-              | SOME (dep as {master = (thy_path, _), ...}) =>
-                  let
-                    val text = (case opt_text of SOME text => text | NONE => File.read thy_path);
-                    val update_time = serial ();
+              | SOME (dep, text) =>
+                  let val update_time = serial ()
                   in Task (parents, load_thy initiators update_time dep text name) end);
         in (all_current, new_entry name parents task tasks') end)
   end;
 
 end;

 (* register theory *)
 
 fun register_thy theory =
   let
     val name = Context.theory_name theory;
-    val master = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
+    val {master, ...} = Thy_Load.check_thy (Thy_Load.master_directory theory) name;
     val parents = map Context.theory_name (Theory.parents_of theory);
     val imports = Thy_Load.imports_of theory;
     val deps = make_deps master imports;
   in
     NAMED_CRITICAL "Thy_Info" (fn () =>