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