--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Sep 13 14:29:53 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Mon Sep 13 14:30:21 2010 +0200
@@ -81,7 +81,7 @@
fun sublinear_minimize _ [] p = p
| sublinear_minimize test (x :: xs) (seen, result) =
case test (xs @ seen) of
- result as {outcome = NONE, proof, used_thm_names, ...} : prover_result =>
+ result as {outcome = NONE, used_thm_names, ...} : prover_result =>
sublinear_minimize test (filter_used_facts used_thm_names xs)
(filter_used_facts used_thm_names seen, result)
| _ => sublinear_minimize test xs (x :: seen, result)
@@ -94,7 +94,7 @@
fun minimize_theorems {atps = [], ...} _ _ _ _ = error "No ATP is set."
| minimize_theorems (params as {debug, atps = atp :: _, full_types,
isar_proof, isar_shrink_factor, timeout, ...})
- i n state axioms =
+ i (_ : int) state axioms =
let
val thy = Proof.theory_of state
val prover = get_prover_fun thy atp