1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sun Feb 02 20:53:51 2014 +0100
     1.3 @@ -137,6 +137,7 @@
     1.4  
     1.5          val do_preplay = preplay_timeout <> Time.zeroTime
     1.6          val try0_isar = try0_isar andalso do_preplay
     1.7 +        val compress_isar = if isar_proofs = NONE andalso do_preplay then 1000.0 else compress_isar
     1.8  
     1.9          val is_fixed = Variable.is_declared ctxt orf can Name.dest_skolem
    1.10          fun skolems_of t = Term.add_frees t [] |> filter_out (is_fixed o fst) |> rev
    1.11 @@ -279,8 +280,8 @@
    1.12            |> relabel_isar_proof_canonically
    1.13  
    1.14          val preplay_data as {preplay_outcome, overall_preplay_outcome, ...} =
    1.15 -          preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans do_preplay
    1.16 -            preplay_timeout isar_proof
    1.17 +          preplay_data_of_isar_proof debug ctxt metis_type_enc metis_lam_trans preplay_timeout
    1.18 +            isar_proof
    1.19  
    1.20          fun str_of_preplay_outcome outcome =
    1.21            if Lazy.is_finished outcome then string_of_play_outcome (Lazy.force outcome) else "?"
    1.22 @@ -299,8 +300,7 @@
    1.23          val (play_outcome, isar_proof) =
    1.24            isar_proof
    1.25            |> tap (trace_isar_proof "Original")
    1.26 -          |> compress_isar_proof (if isar_proofs = SOME true then compress_isar else 1000.0)
    1.27 -               preplay_data
    1.28 +          |> compress_isar_proof compress_isar preplay_data
    1.29            |> tap (trace_isar_proof "Compressed")
    1.30            |> try0_isar ? try0_isar_proof preplay_timeout preplay_data
    1.31            |> tap (trace_isar_proof "Tried0")