use rpair to avoid swap
authorsmolkas
Wed, 02 Jan 2013 20:35:49 +0100
changeset 50677 f5c217474eca
parent 50676 83b8a5a39709
child 50678 027c09d7f6ec
use rpair to avoid swap
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML
--- 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