# HG changeset patch
# User blanchet
# Date 1304267844 -7200
# Node ID f83036b85a3aec5ebab51d43ad17ae5610d45d76
# Parent  d9963b253ffa4e41e108eeb5e62587470a850a0b
added friendly hint when Isar proof is missing

diff -r d9963b253ffa -r f83036b85a3a src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
--- 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