prefer uniform Timing.message -- avoid assumption about sequential execution;
authorwenzelm
Mon Feb 27 17:39:34 2012 +0100 (2012-02-27)
changeset 46713e6e1ec6d5c1c
parent 46712 8650d9a95736
child 46714 a7ca72710dfe
prefer uniform Timing.message -- avoid assumption about sequential execution;
src/HOL/Tools/Quickcheck/find_unused_assms.ML
src/Pure/Tools/find_consts.ML
src/Pure/Tools/find_theorems.ML
     1.1 --- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 17:13:25 2012 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 17:39:34 2012 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4      val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
     1.5        ^ " in the theory " ^ quote thy_name
     1.6        ^ " with a total of " ^ string_of_int total ^ " theorem(s)"  
     1.7 -      ^ " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
     1.8 +      ^ " in " ^ Timing.message (Timing.result start);
     1.9    in
    1.10      ([Pretty.str (msg ^ ":"), Pretty.str ""] @
    1.11          map pretty_thm with_superfluous_assumptions
     2.1 --- a/src/Pure/Tools/find_consts.ML	Mon Feb 27 17:13:25 2012 +0100
     2.2 +++ b/src/Pure/Tools/find_consts.ML	Mon Feb 27 17:39:34 2012 +0100
     2.3 @@ -114,7 +114,7 @@
     2.4        |> sort (rev_order o int_ord o pairself snd)
     2.5        |> map (apsnd fst o fst);
     2.6  
     2.7 -    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
     2.8 +    val end_msg = " in " ^ Timing.message (Timing.result start);
     2.9    in
    2.10      Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
    2.11      Pretty.str "" ::
     3.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 17:13:25 2012 +0100
     3.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 17:39:34 2012 +0100
     3.3 @@ -602,7 +602,7 @@
     3.4               then " (" ^ string_of_int returned ^ " displayed)"
     3.5               else ""));
     3.6  
     3.7 -    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
     3.8 +    val end_msg = " in " ^ Timing.message (Timing.result start);
     3.9    in
    3.10      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
    3.11      Pretty.str "" ::