removed hint that is seldom useful in practice
authorblanchet
Thu Feb 13 13:16:16 2014 +0100 (2014-02-13)
changeset 55451ea1d9408a233
parent 55450 9eddc17749f7
child 55452 29ec8680e61f
removed hint that is seldom useful in practice
src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 12:24:28 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Thu Feb 13 13:16:16 2014 +0100
     1.3 @@ -183,11 +183,8 @@
     1.4      val try_line =
     1.5        map fst extra
     1.6        |> proof_method_command meth subgoal subgoal_count (map fst chained) num_chained
     1.7 -      |> (if failed then
     1.8 -            enclose "One-line proof reconstruction failed: "
     1.9 -              ".\n(Invoking \"sledgehammer\" with \"[strict]\" might solve this.)"
    1.10 -          else
    1.11 -            try_command_line banner ext_time)
    1.12 +      |> (if failed then enclose "One-line proof reconstruction failed: " "."
    1.13 +          else try_command_line banner ext_time)
    1.14    in
    1.15      try_line ^ minimize_line minimize_command (map fst (extra @ chained))
    1.16    end