# HG changeset patch
# User wenzelm
# Date 1197930387 -3600
# Node ID c36e10812ae4a4822d9882b2c2bdc8d3429871b0
# Parent  2b3cce7d22b87b3c6f09d115df293584d8e5f5ba
cond_timeit: added message argument;

diff -r 2b3cce7d22b8 -r c36e10812ae4 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Mon Dec 17 22:40:14 2007 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Mon Dec 17 23:26:27 2007 +0100
@@ -304,7 +304,7 @@
       |> Source.exhaust;
 
     val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
-    val _ = cond_timeit time (fn () =>
+    val _ = cond_timeit time "" (fn () =>
       ThyOutput.process_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
       |> Buffer.content
       |> Present.theory_output name);
diff -r 2b3cce7d22b8 -r c36e10812ae4 src/Pure/old_goals.ML
--- a/src/Pure/old_goals.ML	Mon Dec 17 22:40:14 2007 +0100
+++ b/src/Pure/old_goals.ML	Mon Dec 17 23:26:27 2007 +0100
@@ -228,7 +228,7 @@
           (case Seq.pull (tac st0) of
                SOME(st,_) => st
              | _ => error ("prove_goal: tactic failed"))
-  in  mkresult (check, cond_timeit (!Output.timing) statef)  end
+  in  mkresult (check, cond_timeit (!Output.timing) "" statef)  end
   handle e => (print_sign_exn_unit (#thy (rep_cterm chorn)) e;
                writeln ("The exception above was raised for\n" ^
                       Display.string_of_cterm chorn); raise e);
@@ -402,7 +402,7 @@
                        thy_error (Thm.theory_of_thm th, Thm.theory_of_thm th2));
        ((th2,ths2)::(th,ths)::pairs)));
 
-fun by tac = cond_timeit (!Output.timing)
+fun by tac = cond_timeit (!Output.timing) ""
     (fn() => make_command (by_com tac));
 
 (* byev[tac1,...,tacn] applies tac1 THEN ... THEN tacn.