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
             ""
         | _ =>