--- a/doc-src/Sledgehammer/sledgehammer.tex Sat Feb 04 12:08:18 2012 +0100
+++ b/doc-src/Sledgehammer/sledgehammer.tex Sat Feb 04 12:08:18 2012 +0100
@@ -1007,8 +1007,8 @@
irrespective of the value of this option.
\opsmartx{uncurried\_aliases}{no\_uncurried\_aliases}
-Specifies the $\lambda$ translation scheme to use in ATP problems. The supported
-translation schemes are listed below:
+Specifies whether fresh function symbols should be generated as aliases for
+applications of curried functions in ATP problems.
\opdefault{type\_enc}{string}{smart}
Specifies the type encoding to use in ATP problems. Some of the type encodings