src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
changeset 50276 1db687c43663
parent 50274 2f6035e858b6
child 50277 e0a4d8404c76
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Nov 28 12:25:43 2012 +0100
@@ -716,10 +716,10 @@
         | _ =>
           let 
             val preplay_msg = if preplay_fail
-              then "(!) proof may fail - preplaying was unsuccessful"
+              then "may fail"
               else string_from_ext_time ext_time
             val shrank_without_preplay_msg =
-              "(!) proof may fail - shrank proof, but did not preplay"
+              "may fail - shrank proof, but did not preplay"
             in
               "\n\nStructured proof"
                 ^ (if verbose then