--- 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),
--- 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 =