# HG changeset patch
# User blanchet
# Date 1357421490 -3600
# Node ID a057d3fd678395327bc826ae95139489982d1a5b
# Parent  6e7e8e3107978a4bcba48224bdcc938aa8678427
pass option to minimize

diff -r 6e7e8e310797 -r a057d3fd6783 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jan 05 22:02:44 2013 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Jan 05 22:31:30 2013 +0100
@@ -119,7 +119,7 @@
 val params_for_minimize =
   ["debug", "verbose", "overlord", "type_enc", "strict", "lam_trans",
    "uncurried_aliases", "max_mono_iters", "max_new_mono_instances",
-   "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
+   "learn", "isar_proofs", "isar_shrink", "timeout", "preplay_timeout"]
 
 val property_dependent_params = ["provers", "timeout"]