# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID 1db687c43663cbe18380297640eff9445d0eab05
# Parent  66cdf5c9b6c72f3631ac5f17854eb3a4e2c3b30f
adapted sledgehammer warnings

diff -r 66cdf5c9b6c7 -r 1db687c43663 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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