# HG changeset patch
# User blanchet
# Date 1381946123 -7200
# Node ID 2c13cb4a057de664e094b4b0d1acf96dc869cf58
# Parent  f5fc8525838fd6583f0d2e0f7e0e538764c9d38a
have MaSh minimize

diff -r f5fc8525838f -r 2c13cb4a057d 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