1.1 --- a/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 27 16:59:13 2012 +0300
     1.2 +++ b/src/HOL/Tools/ATP/atp_proof_reconstruct.ML	Tue Mar 27 16:59:13 2012 +0300
     1.3 @@ -270,8 +270,12 @@
     1.4      val try_line =
     1.5        ([], map fst extra)
     1.6        |> reconstructor_command reconstr subgoal subgoal_count
     1.7 -      |> (if failed then enclose "One-line proof reconstruction failed: " "."
     1.8 -          else try_command_line banner ext_time)
     1.9 +      |> (if failed then
    1.10 +            enclose "One-line proof reconstruction failed: "
    1.11 +                     ".\n(Invoking \"sledgehammer\" with \"[strict]\" might \
    1.12 +                     \solve this.)"
    1.13 +          else
    1.14 +            try_command_line banner ext_time)
    1.15    in try_line ^ minimize_line minimize_command (map fst (extra @ chained)) end
    1.16  
    1.17  (** Hard-core proof reconstruction: structured Isar proofs **)