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