--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri May 14 22:28:39 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimizer.ML Fri May 14 22:29:50 2010 +0200
@@ -69,7 +69,7 @@
(* minimalization of thms *)
fun minimize_theorems (params as {debug, atps, full_types, minimize_timeout,
- isar_proof, shrink_factor, ...})
+ isar_proof, isar_shrink_factor, ...})
i n state name_thms_pairs =
let
val thy = Proof.theory_of state
@@ -110,7 +110,8 @@
in
(SOME min_thms,
proof_text isar_proof
- (pool, debug, full_types, shrink_factor, ctxt, conjecture_shape)
+ (pool, debug, full_types, isar_shrink_factor, ctxt,
+ conjecture_shape)
(K "", proof, internal_thm_names, goal, i) |> fst)
end
| {outcome = SOME TimedOut, ...} =>