diff -r 111592b342e2 -r 95b2626c75a8 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 18:51:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 21:14:06 2011 +0200
@@ -361,15 +361,15 @@
     val command = Path.explode (getenv (fst exec) ^ "/" ^ snd exec)
     fun split_time s =
       let
-        val split = String.tokens (fn c => str c = "\n");
-        val (output, t) = s |> split |> split_last |> apfst cat_lines;
-        fun as_num f = f >> (fst o read_int);
-        val num = as_num (Scan.many1 Symbol.is_ascii_digit);
-        val digit = Scan.one Symbol.is_ascii_digit;
-        val num3 = as_num (digit ::: digit ::: (digit >> single));
-        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b);
+        val split = String.tokens (fn c => str c = "\n")
+        val (output, t) = s |> split |> split_last |> apfst cat_lines
+        fun as_num f = f >> (fst o read_int)
+        val num = as_num (Scan.many1 Symbol.is_ascii_digit)
+        val digit = Scan.one Symbol.is_ascii_digit
+        val num3 = as_num (digit ::: digit ::: (digit >> single))
+        val time = num --| Scan.$$ "." -- num3 >> (fn (a, b) => a * 1000 + b)
         val as_time = Scan.read Symbol.stopper time o raw_explode
-      in (output, as_time t) end;
+      in (output, as_time t) end
     fun run_on prob_file =
       case filter (curry (op =) "" o getenv o fst) (exec :: required_execs) of
         (home_var, _) :: _ =>