1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Feb 20 19:57:17 2013 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Feb 21 10:52:14 2013 +0100
     1.3 @@ -718,9 +718,10 @@
     1.4          val (body_trs, end_tr) = split_last proof_trs;
     1.5          val finish = Context.Theory o Proof_Context.theory_of;
     1.6  
     1.7 -        val timing_estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
     1.8 -        val timing_order = Real.floor (Real.max (Math.log10 (Time.toReal timing_estimate), ~3.0));
     1.9 -        val pri = Int.min (timing_order - 3, ~1);
    1.10 +        val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime;
    1.11 +        val pri =
    1.12 +          if estimate = Time.zeroTime then ~1
    1.13 +	  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    1.14  
    1.15          val future_proof = Proof.global_future_proof
    1.16            (fn prf =>