1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Apr 21 18:47:22 2011 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Thu Apr 21 18:51:22 2011 +0200
     1.3 @@ -376,8 +376,8 @@
     1.4  
     1.5  fun auto_sledgehammer state =
     1.6    let val ctxt = Proof.context_of state in
     1.7 -    run_sledgehammer (get_params true ctxt []) true 1
     1.8 -                     no_relevance_override (minimize_command [] 1) state
     1.9 +    run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
    1.10 +                     (minimize_command [] 1) state
    1.11    end
    1.12  
    1.13  val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 18:47:22 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Apr 21 18:51:22 2011 +0200
     2.3 @@ -130,8 +130,7 @@
     2.4    is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
     2.5  
     2.6  fun get_slices slicing slices =
     2.7 -  (0 upto length slices - 1) ~~ slices
     2.8 -  |> not slicing ? (List.last #> single)
     2.9 +  (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
    2.10  
    2.11  fun default_max_relevant_for_prover ctxt slicing name =
    2.12    let val thy = Proof_Context.theory_of ctxt in