# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID 316d94b4ffe2565c073ac0074d503595eeed8070
# Parent  2be84eaf7ebb2d4989eb518cef8f03345888e072
added warning when shrinking proof without preplaying

diff -r 2be84eaf7ebb -r 316d94b4ffe2 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
@@ -718,15 +718,23 @@
             val preplay_msg = if preplay_fail
               then "(!) proof may fail - preplaying was unsuccessful"
               else string_from_ext_time ext_time
+            val shrank_without_preplay_msg =
+              "(!) proof may fail - shrank proof, but did not preplay"
             in
               "\n\nStructured proof"
                 ^ (if verbose then
                     " (" ^ string_of_int num_steps 
                          ^ " metis step" ^ plural_s num_steps
-                          |> preplay ? suffix (", " ^ preplay_msg)
-                          |> suffix ")"
+                         |> (if preplay then 
+                               suffix (", " ^ preplay_msg)
+                             else if isar_shrink > 1.0 then
+                               suffix (", " ^ shrank_without_preplay_msg)
+                             else I)
+                         |> suffix ")"
                    else if preplay then
                      " (" ^ preplay_msg ^ ")"
+                   else if isar_shrink > 1.0 then
+                     " (" ^ shrank_without_preplay_msg ^ ")"
                    else
                      "") 
                 ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text