# HG changeset patch # User wenzelm # Date 1361540332 -3600 # Node ID 67cc209493b252a59eba1fcf6a1a9b6f21dc08bd # Parent 20234cf043d1695696d33452c85599d6242c0a00 eliminated hard tabs; diff -r 20234cf043d1 -r 67cc209493b2 src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Feb 22 14:25:52 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof.ML Fri Feb 22 14:38:52 2013 +0100 @@ -8,7 +8,7 @@ signature SLEDGEHAMMER_PROOF = sig - type label = string * int + type label = string * int type facts = label list * string list datatype isar_qualifier = Show | Then diff -r 20234cf043d1 -r 67cc209493b2 src/Pure/Isar/toplevel.ML --- 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 =>