# HG changeset patch
# User blanchet
# Date 1282210248 -7200
# Node ID 968f8cc672cd29110e5f4591c6d2e28fea8de4ab
# Parent  7f510e5449fb6518f6dd927a5448405293a45849
tuning

diff -r 7f510e5449fb -r 968f8cc672cd src/HOL/Tools/ATP/async_manager.ML
--- a/src/HOL/Tools/ATP/async_manager.ML	Thu Aug 19 11:30:32 2010 +0200
+++ b/src/HOL/Tools/ATP/async_manager.ML	Thu Aug 19 11:30:48 2010 +0200
@@ -72,8 +72,8 @@
           val message' =
             desc ^ "\n" ^ message ^
             (if verbose then
-               "Total time: " ^ Int.toString (Time.toMilliseconds
-                                          (Time.- (now, birth_time))) ^ " ms.\n"
+               "\nTotal time: " ^ Int.toString (Time.toMilliseconds
+                                            (Time.- (now, birth_time))) ^ " ms."
              else
                "")
           val messages' = (tool, message') :: messages;
diff -r 7f510e5449fb -r 968f8cc672cd src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 19 11:30:32 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Aug 19 11:30:48 2010 +0200
@@ -334,14 +334,12 @@
         ()
       else
         File.write (Path.explode (Path.implode probfile ^ "_proof")) output
-
     val ((pool, conjecture_shape, axiom_names),
          (output, msecs, proof, outcome)) =
       with_path cleanup export run_on (prob_pathname subgoal)
     val (conjecture_shape, axiom_names) =
       repair_conjecture_shape_and_theorem_names output conjecture_shape
                                                 axiom_names
-
     val (message, used_thm_names) =
       case outcome of
         NONE =>