# HG changeset patch
# User smolkas
# Date 1357155349 -3600
# Node ID f5c217474eca54e2075836ae629724c922328421
# Parent  83b8a5a39709b4fd75ab2dab85057d7d74552ebe
use rpair to avoid swap

diff -r 83b8a5a39709 -r f5c217474eca 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