# HG changeset patch
# User blanchet
# Date 1381965735 -7200
# Node ID da2b75a04da620717d91c8493230c63c960ef212
# Parent  1e6db1c9f14ca030a99fa1497ef936da745c2a69
tuning

diff -r 1e6db1c9f14c -r da2b75a04da6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 17 01:20:40 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML	Thu Oct 17 01:22:15 2013 +0200
@@ -439,7 +439,7 @@
                   term_order |> the_default I)
             #> (Option.map (Config.put ATP_Systems.force_sos)
                   force_sos |> the_default I))
-    val params as {max_facts, slice, ...} =
+    val params as {max_facts, ...} =
       Sledgehammer_Isar.default_params ctxt
          ([("verbose", "true"),
            ("fact_filter", fact_filter),
diff -r 1e6db1c9f14c -r da2b75a04da6 src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Oct 17 01:20:40 2013 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML	Thu Oct 17 01:22:15 2013 +0200
@@ -111,7 +111,7 @@
        let
          val {context = ctxt, facts = chained_ths, goal} = Proof.goal pre
          val prover = AList.lookup (op =) args "prover" |> the_default default_prover
-         val params as {max_facts, slice, ...} =
+         val params as {max_facts, ...} =
            Sledgehammer_Isar.default_params ctxt args
          val default_max_facts = Sledgehammer_Provers.default_max_facts_of_prover ctxt prover
          val is_appropriate_prop =