diff -r 257e01fab4b7 -r c1f0bc7e7d80 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Sat Sep 30 20:54:34 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Sat Sep 30 21:39:17 2006 +0200
@@ -106,7 +106,7 @@
 \begin{mldecls}
   \indexml{Variable.add-fixes}\verb|Variable.add_fixes: |\isasep\isanewline%
 \verb|  string list -> Proof.context -> string list * Proof.context| \\
-  \indexml{Variable.invent-fixes}\verb|Variable.invent_fixes: |\isasep\isanewline%
+  \indexml{Variable.variant-fixes}\verb|Variable.variant_fixes: |\isasep\isanewline%
 \verb|  string list -> Proof.context -> string list * Proof.context| \\
   \indexml{Variable.declare-term}\verb|Variable.declare_term: term -> Proof.context -> Proof.context| \\
   \indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
@@ -126,7 +126,7 @@
   already.  There is a different policy within a local proof body: the
   given names are just hints for newly invented Skolem variables.
 
-  \item \verb|Variable.invent_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given
+  \item \verb|Variable.variant_fixes| is similar to \verb|Variable.add_fixes|, but always produces fresh variants of the given
   names.
 
   \item \verb|Variable.declare_term|~\isa{t\ ctxt} declares term