changeset 51239 | 67cc209493b2 |
parent 51233 | 7b0c723562af |
child 51241 | 83252b0605be |
--- a/src/Pure/Isar/toplevel.ML Fri Feb 22 14:25:52 2013 +0100 +++ b/src/Pure/Isar/toplevel.ML Fri Feb 22 14:38:52 2013 +0100 @@ -721,7 +721,7 @@ val estimate = fold (curry Time.+ o get_timing) proof_trs Time.zeroTime; val pri = if estimate = Time.zeroTime then ~1 - else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1); + else Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1); val future_proof = Proof.global_future_proof (fn prf =>