# HG changeset patch
# User blanchet
# Date 1392293776 -3600
# Node ID ea1d9408a233e8145ecfd3248bbde27595868a02
# Parent  9eddc17749f7650c0b6a1633b8a209d77c1f2659
removed hint that is seldom useful in practice

diff -r 9eddc17749f7 -r ea1d9408a233 src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 12:24:28 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 13:16:16 2014 +0100
@@ -183,11 +183,8 @@
     val try_line =
       map fst extra
       |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
-      |> (if failed then
-            enclose "One-line proof reconstruction failed: "
-              ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
-          else
-            try_command_line banner ext_time)
+      |> (if failed then enclose "One-line proof reconstruction failed: " "."
+          else try_command_line banner ext_time)
   in
     try_line ^ minimize_line minimize_command (map fst (extra @ chained))
   end