--- a/doc-src/IsarImplementation/Thy/Proof.thy Sat Aug 01 00:39:51 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Sat Aug 01 20:34:34 2009 +0200
@@ -94,7 +94,7 @@
@{index_ML Variable.export: "Proof.context -> Proof.context -> thm list -> thm list"} \\
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
@{index_ML Variable.import: "bool -> thm list -> Proof.context ->
- ((ctyp list * cterm list) * thm list) * Proof.context"} \\
+ (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context"} \\
@{index_ML Variable.focus: "cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context"} \\
\end{mldecls}
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Aug 01 00:39:51 2009 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Aug 01 20:34:34 2009 +0200
@@ -112,7 +112,7 @@
\indexdef{}{ML}{Variable.export}\verb|Variable.export: Proof.context -> Proof.context -> thm list -> thm list| \\
\indexdef{}{ML}{Variable.polymorphic}\verb|Variable.polymorphic: Proof.context -> term list -> term list| \\
\indexdef{}{ML}{Variable.import}\verb|Variable.import: bool -> thm list -> Proof.context ->|\isasep\isanewline%
-\verb| ((ctyp list * cterm list) * thm list) * Proof.context| \\
+\verb| (((ctyp * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\
\indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context -> ((string * cterm) list * cterm) * Proof.context| \\
\end{mldecls}