# HG changeset patch
# User wenzelm
# Date 1330368890 -3600
# Node ID c45a4427db391f6ed4f5d4971e897c8970bc0350
# Parent  6236ca7b32a7a3dc60499426eaddc7f566558fcd
discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);

diff -r 6236ca7b32a7 -r c45a4427db39 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 19:53:34 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 19:54:50 2012 +0100
@@ -84,7 +84,6 @@
 
 fun print_unused_assms ctxt opt_thy_name =
   let
-    val start = Timing.start ()
     val thy_name = the_default (Context.theory_name (Proof_Context.theory_of ctxt)) opt_thy_name
     val results = find_unused_assms ctxt thy_name
     val total = length results
@@ -97,7 +96,6 @@
     val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
       ^ " in the theory " ^ quote thy_name
       ^ " with a total of " ^ string_of_int total ^ " theorem(s)"  
-      ^ " in " ^ Timing.message (Timing.result start);
   in
     ([Pretty.str (msg ^ ":"), Pretty.str ""] @
         map pretty_thm with_superfluous_assumptions
diff -r 6236ca7b32a7 -r c45a4427db39 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Mon Feb 27 19:53:34 2012 +0100
+++ b/src/Pure/Tools/find_consts.ML	Mon Feb 27 19:54:50 2012 +0100
@@ -69,8 +69,6 @@
 
 fun find_consts ctxt raw_criteria =
   let
-    val start = Timing.start ();
-
     val thy = Proof_Context.theory_of ctxt;
     val low_ranking = 10000;
 
@@ -113,15 +111,13 @@
       |> map_filter I
       |> sort (rev_order o int_ord o pairself snd)
       |> map (apsnd fst o fst);
-
-    val end_msg = " in " ^ Timing.message (Timing.result start);
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
     Pretty.str "" ::
     Pretty.str
      (if null matches
-      then "nothing found" ^ end_msg
-      else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
+      then "nothing found"
+      else "found " ^ string_of_int (length matches) ^ " constant(s):") ::
     Pretty.str "" ::
     map (pretty_const ctxt) matches
   end |> Pretty.chunks |> Pretty.writeln;
diff -r 6236ca7b32a7 -r c45a4427db39 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 19:53:34 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 19:54:50 2012 +0100
@@ -586,8 +586,6 @@
 
 fun gen_print_theorems find ctxt opt_goal opt_limit rem_dups raw_criteria =
   let
-    val start = Timing.start ();
-
     val criteria = map (apsnd (read_criterion ctxt)) raw_criteria;
     val (foundo, theorems) = find
       {goal=opt_goal, limit=opt_limit, rem_dups=rem_dups, criteria=criteria};
@@ -601,14 +599,12 @@
             (if returned < found
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
-
-    val end_msg = " in " ^ Timing.message (Timing.result start);
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
     Pretty.str "" ::
-    (if null theorems then [Pretty.str ("nothing found" ^ end_msg)]
+    (if null theorems then [Pretty.str "nothing found"]
      else
-      [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
+      [Pretty.str (tally_msg ^ ":"), Pretty.str ""] @
         map (pretty_theorem ctxt) theorems)
   end |> Pretty.chunks |> Pretty.writeln;