# HG changeset patch
# User wenzelm
# Date 1488214229 -3600
# Node ID 05f1b53422983f5ed45f83feda8ad63e1f82a8cd
# Parent  3e9f382fb67e1c9ea8485e64836b3b76ab3dfea8
clarified priority: zero can mean unknown/long or irrelevant/short time;

diff -r 3e9f382fb67e -r 05f1b5342298 src/Pure/Isar/toplevel.ML
--- 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