# HG changeset patch # User blanchet # Date 1357129873 -3600 # Node ID 6632cb8df708cf399c3b4cc3335ef2bd96afaa5a # Parent eaa540986291951d863a7bef8a680c1d57a4fa85 tuning diff -r eaa540986291 -r 6632cb8df708 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 13:14:47 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 13:31:13 2013 +0100 @@ -714,7 +714,7 @@ case isar_text of "" => if isar_proofs then - "\nNo structured proof available (proof too short)." + "\nNo structured proof available (proof too simple)." else "" | _ =>