--- 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"]