src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 55183 17ec4a29ef71
parent 55170 cdb9435e3cae
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 30 14:28:04 2014 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 30 14:37:53 2014 +0100
     1.3 @@ -36,8 +36,8 @@
     1.4       max_mono_iters : int option,
     1.5       max_new_mono_instances : int option,
     1.6       isar_proofs : bool option,
     1.7 -     isar_compress : real,
     1.8 -     isar_try0 : bool,
     1.9 +     compress_isar : real,
    1.10 +     try0_isar : bool,
    1.11       slice : bool,
    1.12       minimize : bool option,
    1.13       timeout : Time.time,
    1.14 @@ -277,8 +277,8 @@
    1.15     max_mono_iters : int option,
    1.16     max_new_mono_instances : int option,
    1.17     isar_proofs : bool option,
    1.18 -   isar_compress : real,
    1.19 -   isar_try0 : bool,
    1.20 +   compress_isar : real,
    1.21 +   try0_isar : bool,
    1.22     slice : bool,
    1.23     minimize : bool option,
    1.24     timeout : Time.time,
    1.25 @@ -546,8 +546,8 @@
    1.26      ({exec, arguments, proof_delims, known_failures, prem_role, best_slices, best_max_mono_iters,
    1.27        best_max_new_mono_instances, ...} : atp_config)
    1.28      (params as {debug, verbose, overlord, type_enc, strict, lam_trans, uncurried_aliases,
    1.29 -       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, isar_compress,
    1.30 -       isar_try0, slice, timeout, preplay_timeout, ...})
    1.31 +       fact_filter, max_facts, max_mono_iters, max_new_mono_instances, isar_proofs, compress_isar,
    1.32 +       try0_isar, slice, timeout, preplay_timeout, ...})
    1.33      minimize_command
    1.34      ({comment, state, goal, subgoal, subgoal_count, factss, ...} : prover_problem) =
    1.35    let
    1.36 @@ -797,8 +797,8 @@
    1.37                        |> introduce_spass_skolem
    1.38                        |> factify_atp_proof fact_names hyp_ts concl_t
    1.39                    in
    1.40 -                    (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, isar_compress,
    1.41 -                     isar_try0, atp_proof, goal)
    1.42 +                    (verbose, metis_type_enc, metis_lam_trans, preplay_timeout, compress_isar,
    1.43 +                     try0_isar, atp_proof, goal)
    1.44                    end
    1.45                  val one_line_params =
    1.46                    (preplay, proof_banner mode name, used_facts,