# HG changeset patch
# User blanchet
# Date 1307700075 -7200
# Node ID 597f31069e1802ab62f5af4eefddcfd563267cec
# Parent  b19d95b4d7365e7bd4c1b915fd214b1b15250626
fewer monomorphic instances are necessary, thanks to Sascha's new monomorphizer -- backed up by Judgment Day

diff -r b19d95b4d736 -r 597f31069e18 doc-src/Sledgehammer/sledgehammer.tex
--- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jun 10 12:01:15 2011 +0200
+++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jun 10 12:01:15 2011 +0200
@@ -1014,7 +1014,7 @@
 empirically found to be appropriate for the prover. A typical value would be
 250.
 
-\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
+\opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
 Specifies the maximum number of monomorphic instances to generate beyond
 \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
 are potentially generated. Whether monomorphization takes place depends on the
diff -r b19d95b4d736 -r 597f31069e18 src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 10 12:01:15 2011 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 10 12:01:15 2011 +0200
@@ -95,7 +95,7 @@
    ("relevance_thresholds", "0.45 0.85"),
    ("max_relevant", "smart"),
    ("max_mono_iters", "3"),
-   ("max_new_mono_instances", "400"),
+   ("max_new_mono_instances", "200"),
    ("isar_proof", "false"),
    ("isar_shrink_factor", "1"),
    ("slicing", "true"),