author | blanchet |
Wed, 16 Oct 2013 19:55:23 +0200 | |
changeset 54119 | 2c13cb4a057d |
parent 54118 | f5fc8525838f |
child 54120 | c2f18fd05414 |
child 54121 | 4e7d71037bb6 |
--- 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