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