profiling: observe no_timing;

--- a/src/Pure/Isar/toplevel.ML	Tue Jun 19 23:15:57 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML	Tue Jun 19 23:15:59 2007 +0200
@@ -680,7 +680,7 @@
 
     val (result, opt_exn) =
        state |> (apply_trans int pos trans
-        |> (if ! profiling > 0 then do_profiling else I)
+        |> (if ! profiling > 0 then do_profiling andalso not no_timing else I)
         |> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I));
     val _ =
       if int andalso not (! quiet) andalso exists (member (op =) print) ("" :: ! print_mode)