src/Pure/Isar/toplevel.ML
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 =>