author | smolkas |
Wed, 02 Jan 2013 20:35:49 +0100 | |
changeset 50677 | f5c217474eca |
parent 50676 | 83b8a5a39709 |
child 50678 | 027c09d7f6ec |
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 19:59:06 2013 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Wed Jan 02 20:35:49 2013 +0100 @@ -744,7 +744,7 @@ |> map (isar_step_of_direct_inf true) |> append assms |> (if not preplay andalso isar_shrink <= 1.0 then - pair (false, (true, seconds 0.0)) #> swap + rpair (false, (true, seconds 0.0)) else shrink_proof debug ctxt type_enc lam_trans preplay preplay_timeout