# 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 =>