1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 01 13:34:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Dec 01 13:34:13 2011 +0100
     1.3 @@ -65,7 +65,7 @@
     1.4         lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01),
     1.5         max_relevant = SOME (length facts), max_mono_iters = max_mono_iters,
     1.6         max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof,
     1.7 -       isar_shrink_factor = isar_shrink_factor, slicing = false,
     1.8 +       isar_shrink_factor = isar_shrink_factor, slice = false,
     1.9         timeout = timeout, preplay_timeout = preplay_timeout, expect = ""}
    1.10      val problem =
    1.11        {state = state, goal = goal, subgoal = i, subgoal_count = n,