--- 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