1.1 --- a/src/Pure/System/session.ML	Sun Mar 20 21:20:07 2011 +0100
     1.2 +++ b/src/Pure/System/session.ML	Sun Mar 20 21:28:11 2011 +0100
     1.3 @@ -101,13 +101,12 @@
     1.4          (dumping dump) (get_rpath rpath) verbose (map Thy_Info.get_theory (Thy_Info.get_names ()));
     1.5        if timing then
     1.6          let
     1.7 -          val start = start_timing ();
     1.8 +          val start = Timing.start ();
     1.9            val _ = use root;
    1.10 -          val stop = end_timing start;
    1.11            val _ =
    1.12              Output.raw_stderr ("Timing " ^ item ^ " (" ^
    1.13                string_of_int (Multithreading.max_threads_value ()) ^ " threads, " ^
    1.14 -              #message stop ^ ")\n");
    1.15 +              Timing.message (Timing.result start) ^ ")\n");
    1.16          in () end
    1.17        else use root;
    1.18        finish ()))