# HG changeset patch
# User blanchet
# Date 1284381021 -7200
# Node ID 9608a5bd5d207c1fb046aa05b3708e3f07de75f1
# Parent  1c2ed6dc44427bac2cc31202a6289ce61dae4395
tuning

diff -r 1c2ed6dc4442 -r 9608a5bd5d20 src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- 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