diff -r 027c09d7f6ec -r e409d9f8ec75 src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 20:52:32 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 20:52:39 2013 +0100 @@ -747,8 +747,8 @@ rpair (false, (true, seconds 0.0)) else shrink_proof debug ctxt type_enc lam_trans preplay - preplay_timeout - (if isar_proofs then isar_shrink else 1000.0)) + preplay_timeout + (if isar_proofs then isar_shrink else 1000.0)) (* |>> reorder_proof_to_minimize_jumps (* ? *) *) |>> chain_direct_proof |>> kill_useless_labels_in_proof