--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 31 21:17:19 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact_minimize.ML Tue Aug 31 22:27:33 2010 +0200
@@ -49,8 +49,8 @@
val _ =
priority ("Testing " ^ n_theorems (map fst axioms) ^ "...")
val params =
- {debug = debug, verbose = verbose, overlord = overlord, atps = atps,
- full_types = full_types, explicit_apply = explicit_apply,
+ {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
+ atps = atps, full_types = full_types, explicit_apply = explicit_apply,
relevance_thresholds = (1.01, 1.01), max_relevant = NONE,
theory_relevant = NONE, isar_proof = isar_proof,
isar_shrink_factor = isar_shrink_factor, timeout = timeout}