don't be overly verbose in Sledgehammer's minimizer
authorblanchet
Wed, 03 Nov 2010 22:33:23 +0100
changeset 40342 3154f63e2bda
parent 40341 03156257040f
child 40343 4521d56aef63
don't be overly verbose in Sledgehammer's minimizer
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,