Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
use rpair to avoid swap
authorsmolkas
Wed, 02 Jan 2013 20:35:49 +0100
changeset 51692f5c217474eca
parent 51691 83b8a5a39709
child 51693 027c09d7f6ec
use rpair to avoid swap
src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML file | annotate | diff | comparison | revisions 
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 19:59:06 2013 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Wed Jan 02 20:35:49 2013 +0100
     1.3 @@ -744,7 +744,7 @@
     1.4            |> map (isar_step_of_direct_inf true)
     1.5            |> append assms
     1.6            |> (if not preplay andalso isar_shrink <= 1.0 then
     1.7 -                pair (false, (true, seconds 0.0)) #> swap
     1.8 +                rpair (false, (true, seconds 0.0))
     1.9                else
    1.10                  shrink_proof debug ctxt type_enc lam_trans preplay
    1.11                      preplay_timeout
wneuper/isa