--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Feb 09 17:18:58 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Thu Feb 10 10:09:38 2011 +0100
@@ -81,7 +81,9 @@
in
print silent (fn () =>
case outcome of
- SOME failure => short_string_for_failure failure
+ SOME failure =>
+ (if verbose then string_for_failure else short_string_for_failure)
+ failure
| NONE =>
if length used_facts = length facts then "Found proof."
else "Found proof with " ^ n_facts used_facts ^ ".");