src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
changeset 50020 6b9611abcd4c
parent 50004 c96e8e40d789
child 50486 d5dc28fafd9d
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 06 15:12:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Nov 06 15:15:33 2012 +0100
     1.3 @@ -34,7 +34,7 @@
     1.4       max_mono_iters : int option,
     1.5       max_new_mono_instances : int option,
     1.6       isar_proofs : bool,
     1.7 -     isar_shrinkage : real,
     1.8 +     isar_shrink : real,
     1.9       slice : bool,
    1.10       minimize : bool option,
    1.11       timeout : Time.time,
    1.12 @@ -327,7 +327,7 @@
    1.13     max_mono_iters : int option,
    1.14     max_new_mono_instances : int option,
    1.15     isar_proofs : bool,
    1.16 -   isar_shrinkage : real,
    1.17 +   isar_shrink : real,
    1.18     slice : bool,
    1.19     minimize : bool option,
    1.20     timeout : Time.time,
    1.21 @@ -642,7 +642,7 @@
    1.22            best_max_mono_iters, best_max_new_mono_instances, ...} : atp_config)
    1.23          (params as {debug, verbose, overlord, type_enc, strict, lam_trans,
    1.24                      uncurried_aliases, max_facts, max_mono_iters,
    1.25 -                    max_new_mono_instances, isar_proofs, isar_shrinkage,
    1.26 +                    max_new_mono_instances, isar_proofs, isar_shrink,
    1.27                      slice, timeout, preplay_timeout, ...})
    1.28          minimize_command
    1.29          ({state, goal, subgoal, subgoal_count, facts, ...} : prover_problem) =
    1.30 @@ -888,7 +888,7 @@
    1.31                    else
    1.32                      ()
    1.33                  val isar_params =
    1.34 -                  (debug, verbose, preplay_timeout, isar_shrinkage,
    1.35 +                  (debug, verbose, preplay_timeout, isar_shrink,
    1.36                     pool, fact_names, sym_tab, atp_proof, goal)
    1.37                  val one_line_params =
    1.38                    (preplay, proof_banner mode name, used_facts,