diff -r 724e612ba248 -r 8e5438dc70bb src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 18:39:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Apr 21 18:39:22 2011 +0200
@@ -14,10 +14,10 @@
   type prover = Sledgehammer_Provers.prover
 
   val auto_minimize_min_facts : int Unsynchronized.ref
-  val get_minimizing_prover : Proof.context -> bool -> bool -> string -> prover
+  val get_minimizing_prover : Proof.context -> bool -> string -> prover
   val run_sledgehammer :
-    params -> bool -> bool -> int -> relevance_override
-    -> (string -> minimize_command) -> Proof.state -> bool * Proof.state
+    params -> bool -> int -> relevance_override -> (string -> minimize_command)
+    -> Proof.state -> bool * Proof.state
 end;
 
 structure Sledgehammer_Run : SLEDGEHAMMER_RUN =
@@ -44,10 +44,10 @@
 
 val auto_minimize_min_facts = Unsynchronized.ref (!binary_min_facts)
 
-fun get_minimizing_prover ctxt auto may_slice name
+fun get_minimizing_prover ctxt auto name
         (params as {debug, verbose, explicit_apply, ...}) minimize_command
         (problem as {state, subgoal, subgoal_count, facts, ...}) =
-  get_prover ctxt auto may_slice name params minimize_command problem
+  get_prover ctxt auto name params minimize_command problem
   |> (fn result as {outcome, used_facts, run_time_in_msecs, message} =>
          if is_some outcome then
            result
@@ -85,11 +85,10 @@
 
 fun launch_prover (params as {debug, blocking, max_relevant, slicing, timeout,
                               expect, ...})
-        auto may_slice minimize_command only
+        auto minimize_command only
         {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
   let
     val ctxt = Proof.context_of state
-    val slicing = may_slice andalso slicing
     val birth_time = Time.now ()
     val death_time = Time.+ (birth_time, timeout)
     val max_relevant =
@@ -104,8 +103,7 @@
        smt_filter = smt_filter}
     fun really_go () =
       problem
-      |> get_minimizing_prover ctxt auto may_slice name params
-                               (minimize_command name)
+      |> get_minimizing_prover ctxt auto name params (minimize_command name)
       |> (fn {outcome, message, ...} =>
              (if is_some outcome then "none" else "some" (* sic *), message))
     fun go () =
@@ -170,8 +168,7 @@
 fun run_sledgehammer (params as {debug, blocking, provers, monomorphize,
                                  type_sys, relevance_thresholds, max_relevant,
                                  slicing, timeout, ...})
-                     auto may_slice i (relevance_override as {only, ...})
-                     minimize_command state =
+        auto i (relevance_override as {only, ...}) minimize_command state =
   if null provers then
     error "No prover is set."
   else case subgoal_count state of
@@ -184,7 +181,6 @@
         state |> Proof.map_context (Config.put SMT_Config.verbose debug)
       val ctxt = Proof.context_of state
       val thy = Proof_Context.theory_of ctxt
-      val slicing = may_slice andalso slicing
       val {facts = chained_ths, goal, ...} = Proof.goal state
       val (_, hyp_ts, concl_t) = strip_subgoal goal i
       val no_dangerous_types = types_dangerous_types type_sys
@@ -205,7 +201,7 @@
              facts = facts,
              smt_filter = maybe_smt_filter
                   (fn () => map_filter (try dest_SMT_Weighted_Fact) facts) i}
-          val launch = launch_prover params auto may_slice minimize_command only
+          val launch = launch_prover params auto minimize_command only
         in
           if auto then
             fold (fn prover => fn (true, state) => (true, state)