have MaSh minimize
authorblanchet
Wed, 16 Oct 2013 19:55:23 +0200
changeset 54119 2c13cb4a057d
parent 54118 f5fc8525838f
child 54120 c2f18fd05414
child 54121 4e7d71037bb6
have MaSh minimize
src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Tue Oct 15 23:00:46 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_minimize.ML	Wed Oct 16 19:55:23 2013 +0200
@@ -314,7 +314,7 @@
                preplay)
             end
         else
-          ((false, (name, params)), preplay)
+          ((mode = MaSh, (name, params)), preplay)
       val minimize = minimize |> the_default perhaps_minimize
       val (used_facts, (preplay, message, _)) =
         if minimize then