diff -r a25ff4283352 -r 418846ea4f99 src/HOL/Tools/Sledgehammer/sledgehammer_run.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML	Thu Dec 01 13:34:13 2011 +0100
@@ -75,8 +75,8 @@
 fun adjust_reconstructor_params override_params
         ({debug, verbose, overlord, blocking, provers, type_enc, sound,
          lam_trans, relevance_thresholds, max_relevant, max_mono_iters,
-         max_new_mono_instances, isar_proof, isar_shrink_factor, slicing,
-         timeout, preplay_timeout, expect} : params) =
+         max_new_mono_instances, isar_proof, isar_shrink_factor, slice, timeout,
+         preplay_timeout, expect} : params) =
   let
     fun lookup_override name default_value =
       case AList.lookup (op =) override_params name of
@@ -93,8 +93,8 @@
      relevance_thresholds = relevance_thresholds,
      max_mono_iters = max_mono_iters,
      max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
-     isar_shrink_factor = isar_shrink_factor, slicing = slicing,
-     timeout = timeout, preplay_timeout = preplay_timeout, expect = expect}
+     isar_shrink_factor = isar_shrink_factor, slice = slice, timeout = timeout,
+     preplay_timeout = preplay_timeout, expect = expect}
   end
 
 fun minimize ctxt mode name (params as {debug, verbose, isar_proof, ...})
@@ -172,7 +172,7 @@
 fun is_induction_fact (Untranslated_Fact ((_, Induction), _)) = true
   | is_induction_fact _ = false
 
-fun launch_prover (params as {debug, verbose, blocking, max_relevant, slicing,
+fun launch_prover (params as {debug, verbose, blocking, max_relevant, slice,
                               timeout, expect, ...})
         mode minimize_command only
         {state, goal, subgoal, subgoal_count, facts, smt_filter} name =
@@ -183,7 +183,7 @@
     val death_time = Time.+ (birth_time, hard_timeout)
     val max_relevant =
       max_relevant
-      |> the_default (default_max_relevant_for_prover ctxt slicing name)
+      |> the_default (default_max_relevant_for_prover ctxt slice name)
     val num_facts = length facts |> not only ? Integer.min max_relevant
     fun desc () =
       prover_description ctxt params name num_facts subgoal subgoal_count goal
@@ -277,7 +277,7 @@
 val auto_try_max_relevant_divisor = 2 (* FUDGE *)
 
 fun run_sledgehammer (params as {debug, verbose, blocking, provers,
-                                 relevance_thresholds, max_relevant, slicing,
+                                 relevance_thresholds, max_relevant, slice,
                                  timeout, ...})
         mode i (relevance_override as {only, ...}) minimize_command state =
   if null provers then
@@ -338,7 +338,7 @@
               SOME n => n
             | NONE =>
               0 |> fold (Integer.max
-                         o default_max_relevant_for_prover ctxt slicing)
+                         o default_max_relevant_for_prover ctxt slice)
                         provers
                 |> mode = Auto_Try
                    ? (fn n => n div auto_try_max_relevant_divisor)