1.1 --- a/doc-src/Sledgehammer/sledgehammer.tex	Fri Jun 10 12:01:15 2011 +0200
     1.2 +++ b/doc-src/Sledgehammer/sledgehammer.tex	Fri Jun 10 12:01:15 2011 +0200
     1.3 @@ -1014,7 +1014,7 @@
     1.4  empirically found to be appropriate for the prover. A typical value would be
     1.5  250.
     1.6  
     1.7 -\opdefault{max\_new\_mono\_instances}{int}{\upshape 400}
     1.8 +\opdefault{max\_new\_mono\_instances}{int}{\upshape 200}
     1.9  Specifies the maximum number of monomorphic instances to generate beyond
    1.10  \textit{max\_relevant}. The higher this limit is, the more monomorphic instances
    1.11  are potentially generated. Whether monomorphization takes place depends on the

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 10 12:01:15 2011 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Fri Jun 10 12:01:15 2011 +0200
     2.3 @@ -95,7 +95,7 @@
     2.4     ("relevance_thresholds", "0.45 0.85"),
     2.5     ("max_relevant", "smart"),
     2.6     ("max_mono_iters", "3"),
     2.7 -   ("max_new_mono_instances", "400"),
     2.8 +   ("max_new_mono_instances", "200"),
     2.9     ("isar_proof", "false"),
    2.10     ("isar_shrink_factor", "1"),
    2.11     ("slicing", "true"),