diff -r 95aeaa3ef35d -r 3469df62fe21 doc-src/IsarImplementation/Thy/proof.thy
--- a/doc-src/IsarImplementation/Thy/proof.thy	Thu Jul 06 16:49:37 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/proof.thy	Thu Jul 06 16:49:38 2006 +0200
@@ -7,6 +7,36 @@
 
 section {* Proof context *}
 
+subsection {* Local variables *}
+
+text %mlref {*
+  \begin{mldecls}
+  @{index_ML Variable.declare_term: "term -> Proof.context -> Proof.context"} \\
+  @{index_ML Variable.import: "bool -> thm list -> Proof.context -> thm list * Proof.context"} \\
+  @{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
+  @{index_ML Variable.trade: "Proof.context -> (thm list -> thm list) -> thm list -> thm list"} \\
+  @{index_ML Variable.monomorphic: "Proof.context -> term list -> term list"} \\
+  @{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
+  \end{mldecls}
+
+  \begin{description}
+
+  \item @{ML Variable.declare_term} FIXME
+
+  \item @{ML Variable.import} FIXME
+
+  \item @{ML Variable.export} FIXME
+
+  \item @{ML Variable.trade} composes @{ML Variable.import} and @{ML
+  Variable.export}.
+
+  \item @{ML Variable.monomorphic} FIXME
+
+  \item @{ML Variable.polymorphic} FIXME
+
+  \end{description}
+*}
+
 text FIXME
 
 section {* Proof state *}