# HG changeset patch
# User blanchet
# Date 1288820003 -3600
# Node ID 3154f63e2bda72b7c2a54046afb897ae42d0e685
# Parent  03156257040f6491bf6b159548a16a7ec9961923
don't be overly verbose in Sledgehammer's minimizer

diff -r 03156257040f -r 3154f63e2bda src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- 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,