diff -r 1565d476a9e2 -r ed7aa5a350ef doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Tue Apr 03 19:24:11 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Tue Apr 03 19:24:13 2007 +0200
@@ -112,7 +112,7 @@
   \indexml{Variable.declare-constraints}\verb|Variable.declare_constraints: term -> Proof.context -> Proof.context| \\
   \indexml{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
   \indexml{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
-  \indexml{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
+  \indexml{Variable.import-thms}\verb|Variable.import_thms: bool -> thm list -> Proof.context ->|\isasep\isanewline%
 \verb|  ((ctyp list * cterm list) * thm list) * Proof.context| \\
   \indexml{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> (cterm list * cterm) * Proof.context| \\
   \end{mldecls}
@@ -150,7 +150,7 @@
   with \verb|Variable.polymorphic|: here the given terms are detached
   from the context as far as possible.
 
-  \item \verb|Variable.import|~\isa{open\ thms\ ctxt} invents fixed
+  \item \verb|Variable.import_thms|~\isa{open\ thms\ ctxt} invents fixed
   type and term variables for the schematic ones occurring in \isa{thms}.  The \isa{open} flag indicates whether the fixed names
   should be accessible to the user, otherwise newly introduced names
   are marked as ``internal'' (\secref{sec:names}).