# HG changeset patch
# User blanchet
# Date 1328353698 -3600
# Node ID cafa325419f6f9421a918c2e1f3d988f59494b7f
# Parent  78ff6a886b50a75a8913942f67efe5c9c20385bd
fixed docs

diff -r 78ff6a886b50 -r cafa325419f6 doc-src/Sledgehammer/sledgehammer.tex
--- 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