src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML
changeset 42554 f83036b85a3a
parent 42551 cd99d6d3027a
child 42562 f1d903f789b1
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_reconstruct.ML	Sun May 01 18:37:24 2011 +0200
     1.3 @@ -972,7 +972,7 @@
     1.4             |> kill_useless_labels_in_proof
     1.5             |> relabel_proof
     1.6             |> string_for_proof ctxt type_sys i n of
     1.7 -        "" => "\nNo structured proof available."
     1.8 +        "" => "\nNo structured proof available (proof too short)."
     1.9        | proof => "\n\nStructured proof:\n" ^ Markup.markup Markup.sendback proof
    1.10      val isar_proof =
    1.11        if debug then