# HG changeset patch
# User blanchet
# Date 1305274244 -7200
# Node ID 226962b6a6d14c27c6cd7101aac3d5799149e84c
# Parent  39ed2de5997a444e04e03c3c84a47effac4d4942
reduce the number of mono iterations to prevent the mono code from going berserk

diff -r 39ed2de5997a -r 226962b6a6d1 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 13 10:10:43 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri May 13 10:10:44 2011 +0200
@@ -82,8 +82,8 @@
    ("type_sys", "smart"),
    ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
-   ("max_mono_iters", "5"),
-   ("max_new_mono_instances", "250"),
+   ("max_mono_iters", "3"),
+   ("max_new_mono_instances", "400"),
    ("explicit_apply", "false"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1"),