--- a/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle_sledgehammer.ML Mon May 02 22:52:15 2011 +0200
@@ -362,7 +362,7 @@
st |> Proof.map_context
(change_dir dir
#> Config.put Sledgehammer_Provers.measure_run_time true)
- val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
+ val params as {relevance_thresholds, max_relevant, slicing, ...} =
Sledgehammer_Isar.default_params ctxt
[("verbose", "true"),
("type_sys", type_sys),
--- 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
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Mon May 02 22:52:15 2011 +0200
@@ -642,7 +642,6 @@
timeout, slicing, ...} : params)
state i smt_filter =
let
- val ctxt = Proof.context_of state
val max_slices = if slicing then !smt_max_slices else 1
val repair_context =
select_smt_solver name
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Mon May 02 22:52:15 2011 +0200
@@ -164,9 +164,8 @@
val auto_max_relevant_divisor = 2 (* FUDGE *)
-fun run_sledgehammer (params as {debug, blocking, provers, type_sys,
- relevance_thresholds, max_relevant, slicing,
- timeout, ...})
+fun run_sledgehammer (params as {debug, blocking, provers, relevance_thresholds,
+ max_relevant, slicing, timeout, ...})
auto i (relevance_override as {only, ...}) minimize_command state =
if null provers then
error "No prover is set."
--- a/src/HOL/ex/sledgehammer_tactics.ML Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/ex/sledgehammer_tactics.ML Mon May 02 22:52:15 2011 +0200
@@ -18,7 +18,7 @@
fun run_atp force_full_types timeout i n ctxt goal name =
let
val chained_ths = [] (* a tactic has no chained ths *)
- val params as {type_sys, relevance_thresholds, max_relevant, slicing, ...} =
+ val params as {relevance_thresholds, max_relevant, slicing, ...} =
((if force_full_types then [("full_types", "true")] else [])
@ [("timeout", string_of_int (Time.toSeconds timeout))])
(* @ [("overlord", "true")] *)
--- a/src/HOL/ex/tptp_export.ML Mon May 02 22:52:15 2011 +0200
+++ b/src/HOL/ex/tptp_export.ML Mon May 02 22:52:15 2011 +0200
@@ -23,7 +23,7 @@
fun facts_of thy =
Sledgehammer_Filter.all_facts (ProofContext.init_global thy) Symtab.empty
- true Sledgehammer_Provers.atp_relevance_fudge [] []
+ true [] []
fun fold_body_thms f =
let