--- a/src/Pure/Isar/toplevel.ML Mon Feb 27 16:29:52 2017 +0100
+++ b/src/Pure/Isar/toplevel.ML Mon Feb 27 17:50:29 2017 +0100
@@ -653,7 +653,8 @@
in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
fun priority estimate =
- Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
+ if estimate = Time.zeroTime then ~1
+ else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1);
fun proof_future_enabled estimate st =
(case try proof_of st of