# HG changeset patch
# User smolkas
# Date 1354101943 -3600
# Node ID e0a4d8404c7681f0eadbf118d418b809d96592fb
# Parent  1db687c43663cbe18380297640eff9445d0eab05
tweaked calculation of sledgehammer messages

diff -r 1db687c43663 -r e0a4d8404c76 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
@@ -702,7 +702,6 @@
           |>> kill_useless_labels_in_proof
           |>> relabel_proof
           |>> not (null params) ? cons (Fix params)
-        val num_steps = metis_steps_total isar_proof
         val isar_text =
           string_for_proof ctxt type_enc lam_trans subgoal subgoal_count
                            isar_proof
@@ -715,30 +714,22 @@
             ""
         | _ =>
           let 
-            val preplay_msg = if preplay_fail
-              then "may fail"
-              else string_from_ext_time ext_time
-            val shrank_without_preplay_msg =
-              "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
-                         |> (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 Markup.sendback isar_text
-            end
+            val msg = 
+              (if preplay then 
+                [if preplay_fail 
+                 then "may fail" 
+                 else string_from_ext_time ext_time]
+               else [])
+              @ 
+               (if verbose then
+                  [let val num_steps = metis_steps_total isar_proof
+                   in string_of_int num_steps ^ plural_s num_steps end]
+                else [])
+          in
+            "\n\nStructured proof "
+              ^ (commas msg |> not (null msg) ? enclose "(" ")")
+              ^ ":\n" ^ Markup.markup Markup.sendback isar_text
+          end
       end
     val isar_proof =
       if debug then