src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML

                            isar_proof
       in
         case isar_text of
           "" =>
           if isar_proofs then
-            "\nNo structured proof available (proof too short)."
+            "\nNo structured proof available (proof too simple)."
           else
             ""
         | _ =>
           let
             val msg =