--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 21 18:47:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Thu Apr 21 18:51:22 2011 +0200
@@ -376,8 +376,8 @@
fun auto_sledgehammer state =
let val ctxt = Proof.context_of state in
- run_sledgehammer (get_params true ctxt []) true 1
- no_relevance_override (minimize_command [] 1) state
+ run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
+ (minimize_command [] 1) state
end
val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 18:47:22 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Thu Apr 21 18:51:22 2011 +0200
@@ -130,8 +130,7 @@
is_smt_prover ctxt orf is_atp_installed (Proof_Context.theory_of ctxt)
fun get_slices slicing slices =
- (0 upto length slices - 1) ~~ slices
- |> not slicing ? (List.last #> single)
+ (0 upto length slices - 1) ~~ slices |> not slicing ? (List.last #> single)
fun default_max_relevant_for_prover ctxt slicing name =
let val thy = Proof_Context.theory_of ctxt in