1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 18:39:22 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 18:39:22 2011 +0200
     1.3 @@ -14,10 +14,10 @@
     1.4    type prover = Sledgehammer_Provers.prover
     1.5  
     1.6    val auto_minimize_min_facts : int Unsynchronized.ref
     1.7 -  val get_minimizing_prover : Proof.context -> bool -> bool -> string -> prover
     1.8 +  val get_minimizing_prover : Proof.context -> bool -> string -> prover
     1.9    val run_sledgehammer :
    1.10 -    params -> bool -> bool -> int -> relevance_override
    1.11 -    -> (string -> minimize_command) -> Proof.state -> bool * Proof.state
    1.12 +    params -> bool -> int -> relevance_override -> (string -> minimize_command)
    1.13 +    -> Proof.state -> bool * Proof.state
    1.14  end;
    1.15  
    1.16  structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
    1.17 @@ -44,10 +44,10 @@
    1.18  
    1.19  val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
    1.20  
    1.21 -fun get_minimizing_prover ctxt auto may_slice name
    1.22 +fun get_minimizing_prover ctxt auto name
    1.23          (params as {debug, verbose, explicit_apply, ...}) minimize_command
    1.24          (problem as {state, subgoal, subgoal_count, facts, ...}) =
    1.25 -  get_prover ctxt auto may_slice name params minimize_command problem
    1.26 +  get_prover ctxt auto name params minimize_command problem
    1.27    |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
    1.28           if is_some outcome then
    1.29             result
    1.30 @@ -85,11 +85,10 @@
    1.31  
    1.32  fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
    1.33                                expect, ...})
    1.34 -        auto may_slice minimize_command only
    1.35 +        auto minimize_command only
    1.36          {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
    1.37    let
    1.38      val ctxt = Proof.context_of state
    1.39 -    val slicing = may_slice andalso slicing
    1.40      val birth_time = Time.now ()
    1.41      val death_time = Time.+ (birth_time, timeout)
    1.42      val max_relevant =
    1.43 @@ -104,8 +103,7 @@
    1.44         smt_filter = smt_filter}
    1.45      fun really_go () =
    1.46        problem
    1.47 -      |> get_minimizing_prover ctxt auto may_slice name params
    1.48 -                               (minimize_command name)
    1.49 +      |> get_minimizing_prover ctxt auto name params (minimize_command name)
    1.50        |> (fn {outcome, message, ...} =>
    1.51               (if is_some outcome then "none" else "some" (* sic *), message))
    1.52      fun go () =
    1.53 @@ -170,8 +168,7 @@
    1.54  fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
    1.55                                   type_sys, relevance_thresholds, max_relevant,
    1.56                                   slicing, timeout, ...})
    1.57 -                     auto may_slice i (relevance_override as {only, ...})
    1.58 -                     minimize_command state =
    1.59 +        auto i (relevance_override as {only, ...}) minimize_command state =
    1.60    if null provers then
    1.61      error "No prover is set."
    1.62    else case subgoal_count state of
    1.63 @@ -184,7 +181,6 @@
    1.64          state |> Proof.map_context (Config.put SMT_Config.verbose debug)
    1.65        val ctxt = Proof.context_of state
    1.66        val thy = Proof_Context.theory_of ctxt
    1.67 -      val slicing = may_slice andalso slicing
    1.68        val {facts = chained_ths, goal, ...} = Proof.goal state
    1.69        val (_, hyp_ts, concl_t) = strip_subgoal goal i
    1.70        val no_dangerous_types = types_dangerous_types type_sys
    1.71 @@ -205,7 +201,7 @@
    1.72               facts = facts,
    1.73               smt_filter = maybe_smt_filter
    1.74                    (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
    1.75 -          val launch = launch_prover params auto may_slice minimize_command only
    1.76 +          val launch = launch_prover params auto minimize_command only
    1.77          in
    1.78            if auto then
    1.79              fold (fn prover => fn (true, state) => (true, state)