src/Pure/Thy/thy_info.ML

   val master_directory: string -> Path.T
   val remove_thy: string -> unit
   val use_theories:
     {document: bool,
      symbols: HTML.symbols,
-     last_timing: Toplevel.transition -> Time.time option,
+     last_timing: Toplevel.transition -> Time.time,
      master_dir: Path.T} -> (string * Position.T) list -> unit
   val use_thys: (string * Position.T) list -> unit
   val use_thy: string * Position.T -> unit
   val script_thy: Position.T -> string -> theory -> theory
   val register_thy: theory -> unit

   schedule_tasks
     (snd (require_thys document symbols last_timing [] master_dir imports String_Graph.empty));
 
 val use_thys =
   use_theories
-    {document = false, symbols = HTML.no_symbols, last_timing = K NONE, master_dir = Path.current};
+    {document = false, symbols = HTML.no_symbols, last_timing = K Time.zeroTime,
+      master_dir = Path.current};
 
 val use_thy = use_thys o single;
 
 
 (* toplevel scripting -- without maintaining database *)