diff -r 1165e8960f59 -r 1905ebfec373 src/Doc/Sledgehammer/document/root.tex
--- a/src/Doc/Sledgehammer/document/root.tex	Wed Sep 11 09:51:30 2013 +0200
+++ b/src/Doc/Sledgehammer/document/root.tex	Wed Sep 11 10:57:09 2013 +0200
@@ -1098,7 +1098,7 @@
 are potentially generated. Whether monomorphization takes place depends on the
 type encoding used. If the option is set to \textit{smart}, it is set to a value
 that was empirically found to be appropriate for the prover. For most provers,
-this value is 200.
+this value is 100.
 
 \nopagebreak
 {\small See also \textit{type\_enc} (\S\ref{problem-encoding}).}