# HG changeset patch
# User blanchet
# Date 1332856753 -10800
# Node ID bd064bc710854f515e52dfe3955afe8408ea1fbf
# Parent  7276f2b12ff7f4f413147c0c49cc582c374a3037
print a hint

diff -r 7276f2b12ff7 -r bd064bc71085 src/HOL/Tools/ATP/atp_proof_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 27 16:59:13 2012 +0300
+++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 27 16:59:13 2012 +0300
@@ -270,8 +270,12 @@
     val try_line =
       ([], map fst extra)
       |> reconstructor_command reconstr subgoal subgoal_count
-      |> (if failed then enclose "One-line proof reconstruction failed: " "."
-          else try_command_line banner ext_time)
+      |> (if failed then
+            enclose "One-line proof reconstruction failed: "
+                     ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
+                     \solve this.)"
+          else
+            try_command_line banner ext_time)
   in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
 
 (** Hard-core proof reconstruction: structured Isar proofs **)