src/Pure/Isar/toplevel.ML
changeset 65059 05f1b5342298
parent 65058 3e9f382fb67e
child 65948 de7888573ed7
     1.1 --- a/src/Pure/Isar/toplevel.ML	Mon Feb 27 16:29:52 2017 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Mon Feb 27 17:50:29 2017 +0100
     1.3 @@ -653,7 +653,8 @@
     1.4    in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
     1.5  
     1.6  fun priority estimate =
     1.7 -  Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
     1.8 +  if estimate = Time.zeroTime then ~1
     1.9 +  else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
    1.10  
    1.11  fun proof_future_enabled estimate st =
    1.12    (case try proof_of st of