# HG changeset patch
# User blanchet
# Date 1352211151 -3600
# Node ID 930a10e674ef485f79e2fbece646ca4995ff2b4d
# Parent  4ea26c74d7eaabf927bbcf48a39b268b716d5280
always show timing for structured proofs

diff -r 4ea26c74d7ea -r 930a10e674ef src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 14:46:21 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Tue Nov 06 15:12:31 2012 +0100
@@ -1029,12 +1029,9 @@
           |> redirect_graph axioms tainted
           |> map (do_inf true)
           |> append assms
-          |> (if isar_shrinkage <= 1.0 andalso isar_proofs then
-                pair (true, seconds 0.0)
-              else
-                shrink_proof debug ctxt type_enc lam_trans preplay
-                     preplay_timeout
-                     (if isar_proofs then isar_shrinkage else 1000.0))
+          |> shrink_proof debug ctxt type_enc lam_trans preplay
+                 preplay_timeout
+                 (if isar_proofs then isar_shrinkage else 1000.0)
        (* ||> reorder_proof_to_minimize_jumps (* ? *) *)
           ||> chain_direct_proof
           ||> kill_useless_labels_in_proof
@@ -1052,21 +1049,15 @@
           else
             ""
         | _ =>
-          "\n\n" ^
-          (if isar_proofs then
-             "Structured proof" ^
-             (if verbose then
-                " (" ^ string_of_int num_steps ^ " step" ^ plural_s num_steps ^
-                (if preplay andalso isar_shrinkage > 1.0 then
-                   ", " ^ string_from_ext_time ext_time
-                 else
-                   "") ^
-                ")"
-              else
-                "")
+          "\n\nStructured proof" ^
+          (if verbose then
+             " (" ^ string_of_int num_steps ^ " step" ^ plural_s num_steps ^
+             (if preplay then ", " ^ string_from_ext_time ext_time
+              else "") ^ ")"
+           else if preplay then
+             " (" ^ string_from_ext_time ext_time ^ ")"
            else
-             "Perhaps this will work") ^
-          ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
+             "") ^ ":\n" ^ Markup.markup Isabelle_Markup.sendback isar_text
       end
     val isar_proof =
       if debug then