src/HOL/Tools/Nunchaku/nunchaku.ML

       timeout_params = {timeout, wf_timeout}})
     mode i all_assms subgoal =
   let
     val ctxt = Proof.context_of state;
 
-    val timer = Timer.startRealTimer ()
+    val time_start = Time.now ()
 
     val print = writeln;
     val print_n = if mode = Normal then writeln else K ();
     fun print_v f = if verbose then writeln (f ()) else ();
     fun print_d f = if debug then writeln (f ()) else ();

       end;
 
     val _ = spying spy (fn () => (state, i, "starting " ^ str_of_mode mode ^ " mode"));
 
     val outcome as (outcome_code, _) =
-      Timeout.apply (Time.+ (timeout, timeout_slack)) run ()
+      Timeout.apply (timeout + timeout_slack) run ()
       handle Timeout.TIMEOUT _ => (print_n "Time out"; (unknownN, NONE));
 
-    val _ = print_v (fn () => "Total time: " ^ string_of_time (Timer.checkRealTimer timer));
+    val _ = print_v (fn () => "Total time: " ^ string_of_time (Time.now () - time_start));
 
     val _ = spying spy (fn () => (state, i, "outcome: " ^ outcome_code));
   in
     if expect = "" orelse outcome_code = expect then outcome
     else error ("Unexpected outcome: " ^ quote outcome_code)