--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:05:22 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Wed Aug 25 09:32:43 2010 +0200
@@ -41,8 +41,8 @@
end
fun test_theorems ({debug, verbose, overlord, atps, full_types,
- relevance_threshold, relevance_decay, defs_relevant,
- isar_proof, isar_shrink_factor, ...} : params)
+ relevance_threshold, relevance_decay, isar_proof,
+ isar_shrink_factor, ...} : params)
(prover : prover) explicit_apply timeout subgoal state
name_thms_pairs =
let
@@ -53,9 +53,8 @@
full_types = full_types, explicit_apply = explicit_apply,
relevance_threshold = relevance_threshold,
relevance_decay = relevance_decay, max_relevant_per_iter = NONE,
- theory_relevant = NONE, defs_relevant = defs_relevant,
- isar_proof = isar_proof, isar_shrink_factor = isar_shrink_factor,
- timeout = timeout}
+ theory_relevant = NONE, isar_proof = isar_proof,
+ isar_shrink_factor = isar_shrink_factor, timeout = timeout}
val axioms = maps (fn (n, ths) => map (pair n) ths) name_thms_pairs
val {context = ctxt, facts, goal} = Proof.goal state
val problem =