src/Pure/Thy/thy_info.ML

 fun load_file time path =
   if time then
     let val name = Path.pack path in
       timeit (fn () =>
        (writeln ("\n**** Starting file " ^ quote name ^ " ****");
-        run_file path;
+        setmp Library.timing true run_file path;
         writeln ("**** Finished file " ^ quote name ^ " ****\n")))
     end
   else run_file path;
 
 val use = load_file false o Path.unpack;

                 if master <> master' then (false, load_deps ml dir name)
                 else (not outdated andalso forall file_current files, same_deps)
               end)
       end);
 
-fun require_thy ml time strict keep_strict initiators prfx (visited, str) =
+fun require_thy ml time_arg strict keep_strict initiators prfx (visited, str) =
   let
     val path = Path.expand (Path.unpack str);
     val name = Path.pack (Path.base path);
+    val time = time_arg orelse ! Library.timing;
   in
     if name mem_string initiators then error (cycle_msg name initiators) else ();
     if known_thy name andalso is_finished name orelse name mem_string visited then
       (visited, (true, name))
     else