verbose minimization when learning from ATP proofs
authorblanchet
Thu, 17 Oct 2013 01:20:40 +0200
changeset 54127 1e6db1c9f14c
parent 54126 6675cdc0d1ae
child 54128 da2b75a04da6
verbose minimization when learning from ATP proofs
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