1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:13 2011 +0100
     1.3 @@ -75,8 +75,8 @@
     1.4  fun adjust_reconstructor_params override_params
     1.5          ({debug, verbose, overlord, blocking, provers, type_enc, sound,
     1.6           lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
     1.7 -         max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
     1.8 -         timeout, preplay_timeout, expect} : params) =
     1.9 +         max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout,
    1.10 +         preplay_timeout, expect} : params) =
    1.11    let
    1.12      fun lookup_override name default_value =
    1.13        case AList.lookup (op =) override_params name of
    1.14 @@ -93,8 +93,8 @@
    1.15       relevance_thresholds = relevance_thresholds,
    1.16       max_mono_iters = max_mono_iters,
    1.17       max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
    1.18 -     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
    1.19 -     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
    1.20 +     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
    1.21 +     preplay_timeout = preplay_timeout, expect = expect}
    1.22    end
    1.23  
    1.24  fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
    1.25 @@ -172,7 +172,7 @@
    1.26  fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
    1.27    | is_induction_fact _ = false
    1.28  
    1.29 -fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
    1.30 +fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
    1.31                                timeout, expect, ...})
    1.32          mode minimize_command only
    1.33          {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
    1.34 @@ -183,7 +183,7 @@
    1.35      val death_time = Time.+ (birth_time, hard_timeout)
    1.36      val max_relevant =
    1.37        max_relevant
    1.38 -      |> the_default (default_max_relevant_for_prover ctxt slicing name)
    1.39 +      |> the_default (default_max_relevant_for_prover ctxt slice name)
    1.40      val num_facts = length facts |> not only ? Integer.min max_relevant
    1.41      fun desc () =
    1.42        prover_description ctxt params name num_facts subgoal subgoal_count goal
    1.43 @@ -277,7 +277,7 @@
    1.44  val auto_try_max_relevant_divisor = 2 (* FUDGE *)
    1.45  
    1.46  fun run_sledgehammer (params as {debug, verbose, blocking, provers,
    1.47 -                                 relevance_thresholds, max_relevant, slicing,
    1.48 +                                 relevance_thresholds, max_relevant, slice,
    1.49                                   timeout, ...})
    1.50          mode i (relevance_override as {only, ...}) minimize_command state =
    1.51    if null provers then
    1.52 @@ -338,7 +338,7 @@
    1.53                SOME n => n
    1.54              | NONE =>
    1.55                0 |> fold (Integer.max
    1.56 -                         o default_max_relevant_for_prover ctxt slicing)
    1.57 +                         o default_max_relevant_for_prover ctxt slice)
    1.58                          provers
    1.59                  |> mode = Auto_Try
    1.60                     ? (fn n => n div auto_try_max_relevant_divisor)