# HG changeset patch
# User blanchet
# Date 1303404682 -7200
# Node ID 111592b342e27d52606993ef04a34a9ac532dea0
# Parent  d105b1309a8d7b0fa9842829dc5834e0eca54b19
tuning

diff -r d105b1309a8d -r 111592b342e2 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- 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)
diff -r d105b1309a8d -r 111592b342e2 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- 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