--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 03 22:26:53 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML Wed Nov 03 22:33:23 2010 +0100
@@ -42,14 +42,14 @@
"")
end
-fun test_facts ({debug, verbose, overlord, provers, full_types, isar_proof,
+fun test_facts ({debug, overlord, provers, full_types, isar_proof,
isar_shrink_factor, ...} : params) (prover : prover)
explicit_apply timeout i n state facts =
let
val _ =
Output.urgent_message ("Testing " ^ n_facts (map fst facts) ^ "...")
val params =
- {blocking = true, debug = debug, verbose = verbose, overlord = overlord,
+ {blocking = true, debug = debug, verbose = false, overlord = overlord,
provers = provers, full_types = full_types,
explicit_apply = explicit_apply, relevance_thresholds = (1.01, 1.01),
max_relevant = NONE, isar_proof = isar_proof,