--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML Sun May 01 18:37:24 2011 +0200
@@ -972,7 +972,7 @@
|> kill_useless_labels_in_proof
|> relabel_proof
|> string_for_proof ctxt type_sys i n of
- "" => "\nNo structured proof available."
+ "" => "\nNo structured proof available (proof too short)."
| proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
val isar_proof =
if debug then