# 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"),