src/Pure/Tools/find_consts.ML
changeset 42012 2c3fe3cbebae
parent 38336 fd53ae1d4c47
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Tools/find_consts.ML	Sun Mar 20 21:20:07 2011 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Sun Mar 20 21:28:11 2011 +0100
     1.3 @@ -69,7 +69,7 @@
     1.4  
     1.5  fun find_consts ctxt raw_criteria =
     1.6    let
     1.7 -    val start = start_timing ();
     1.8 +    val start = Timing.start ();
     1.9  
    1.10      val thy = ProofContext.theory_of ctxt;
    1.11      val low_ranking = 10000;
    1.12 @@ -114,7 +114,7 @@
    1.13        |> sort (rev_order o int_ord o pairself snd)
    1.14        |> map (apsnd fst o fst);
    1.15  
    1.16 -    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
    1.17 +    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
    1.18    in
    1.19      Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
    1.20      Pretty.str "" ::