src/Pure/Thy/thy_info.ML

       fold_map element_result elements (Toplevel.init_toplevel (), Position.none);
 
     val thy = Toplevel.end_theory end_pos end_state;
   in (results, thy) end;
 
-fun eval_thy options update_time master_dir header text_pos text parents =
+fun eval_thy options master_dir header text_pos text parents =
   let
     val (name, _) = #name header;
     val keywords =
       fold (curry Keyword.merge_keywords o Thy_Header.get_keywords) parents
         (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);

 local
 
 fun required_by _ [] = ""
   | required_by s initiators = s ^ "(required by " ^ show_path (rev initiators) ^ ")";
 
-fun load_thy options initiators update_time deps text (name, pos) keywords parents =
+fun load_thy options initiators deps text (name, pos) keywords parents =
   let
     val exec_id = Document_ID.make ();
     val id = Document_ID.print exec_id;
     val _ =
       Execution.running Document_ID.none exec_id [] orelse

     val _ = Output.try_protocol_message (Markup.loading_theory name @ text_props) (XML.blob [text]);
 
     val timing_start = Timing.start ();
 
     val (theory, present, weight) =
-      eval_thy options update_time dir header text_pos text
+      eval_thy options dir header text_pos text
         (if name = Context.PureN then [Context.the_global_context ()] else parents);
 
     val timing_result = Timing.result timing_start;
     val timing_props = [Markup.theory_timing, (Markup.nameN, name)];
     val _  = Output.try_protocol_message (timing_props @ Markup.timing_properties timing_result) []

             if all_current then Finished (get_theory theory_name)
             else
               (case deps of
                 NONE => raise Fail "Malformed deps"
               | SOME (dep, text) =>
-                  let
-                    val update_time = serial ();
-                    val load =
-                      load_thy options initiators update_time
-                        dep text (theory_name, theory_pos) keywords;
-                  in Task (parents, load) end);
+                  Task (parents,
+                    load_thy options initiators dep text (theory_name, theory_pos) keywords));
 
           val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
   end;