--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Sep 11 12:31:05 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Sat Sep 11 12:31:42 2010 +0200
@@ -130,7 +130,8 @@
(SOME min_thms,
proof_text isar_proof
(pool, debug, isar_shrink_factor, ctxt, conjecture_shape)
- (full_types, K "", proof, axiom_names, goal, i) |> fst)
+ ("Minimized command", full_types, K "", proof, axiom_names, goal,
+ i) |> fst)
end
| {outcome = SOME TimedOut, ...} =>
(NONE, "Timeout: You can increase the time limit using the \"timeout\" \