--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML Mon May 02 22:52:15 2011 +0200
@@ -112,7 +112,7 @@
val {context = ctxt, facts, goal} = Proof.goal pre
val prover = AList.lookup (op =) args "prover"
|> the_default default_prover
- val {relevance_thresholds, type_sys, max_relevant, slicing, ...} =
+ val {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt args
val default_max_relevant =
Sledgehammer_Provers.default_max_relevant_for_prover ctxt slicing