# HG changeset patch
# User blanchet
# Date 1391466012 -3600
# Node ID 59ab33f9d4de056dd80d8b67a9bf72889eb2bcd4
# Parent  b1ca6ce9e1e0c8e1be07ac2a307f31801214ca87
tuning

diff -r b1ca6ce9e1e0 -r 59ab33f9d4de src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 19:50:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 23:20:12 2014 +0100
@@ -233,16 +233,17 @@
 
               val succs = collect_successors steps' labels
 
-              (* only touch steps that can be preplayed successfully *)
+              (* only touch steps that can be preplayed successfully; FIXME: more generous *)
               val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l
 
               val succs' = map (try_merge (!preplay_data) cand #> the) succs
 
-              (* FIXME: more generous! *)
+              (* FIXME: more generous *)
               val times0 = map ((fn Played time => time) o
                 forced_intermediate_preplay_outcome_of_isar_step (!preplay_data)) labels
               val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
               val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0
+              (* FIXME: "preplay_timeout" should be an ultimate maximum *)
 
               val meths_outcomess = map2 (preplay_isar_step ctxt) timeouts succs'
 
diff -r b1ca6ce9e1e0 -r 59ab33f9d4de src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 19:50:38 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Mon Feb 03 23:20:12 2014 +0100
@@ -372,7 +372,7 @@
                       |> factify_atp_proof fact_names hyp_ts concl_t
                   in
                     (verbose, (metis_type_enc, metis_lam_trans), preplay_timeout, compress_isar,
-                     try0_isar, minimize |> the_default true, atp_proof, goal)
+                     try0_isar, minimize <> SOME false, atp_proof, goal)
                   end
                 val one_line_params =
                   (preplay, proof_banner mode name, used_facts,