# HG changeset patch
# User blanchet
# Date 1381965640 -7200
# Node ID 1e6db1c9f14ca030a99fa1497ef936da745c2a69
# Parent  6675cdc0d1ae524ba6a8932eeb99b51087ab4f7b
verbose minimization when learning from ATP proofs

diff -r 6675cdc0d1ae -r 1e6db1c9f14c src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 17 01:10:08 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Thu Oct 17 01:20:40 2013 +0200
@@ -314,13 +314,13 @@
                preplay)
             end
         else
-          ((mode = MaSh, (name, params)), preplay)
+          ((false, (name, params)), preplay)
       val minimize = minimize |> the_default perhaps_minimize
       val (used_facts, (preplay, message, _)) =
         if minimize then
           minimize_facts do_learn minimize_name params
-              (mode <> Normal orelse not verbose) subgoal subgoal_count state
-              (SOME preplay)
+              (not verbose orelse (mode <> Normal andalso mode <> MaSh)) subgoal
+              subgoal_count state (SOME preplay)
               (filter_used_facts true used_facts (map (apsnd single) used_from))
           |>> Option.map (map fst)
         else