verbose minimization when learning from ATP proofs

--- 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