--- a/doc-src/IsarImplementation/Thy/Proof.thy Sat Apr 30 23:20:50 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/Proof.thy Sat Apr 30 23:27:57 2011 +0200
@@ -109,8 +109,8 @@
@{index_ML Variable.polymorphic: "Proof.context -> term list -> term list"} \\
@{index_ML Variable.import: "bool -> 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"} \\
+ @{index_ML Variable.focus: "term -> Proof.context ->
+ ((string * (string * typ)) list * term) * Proof.context"} \\
\end{mldecls}
\begin{description}
--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Apr 30 23:20:50 2011 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Sat Apr 30 23:27:57 2011 +0200
@@ -177,8 +177,8 @@
\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 * ctyp) list * (cterm * cterm) list) * thm list) * Proof.context| \\
- \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: cterm -> Proof.context ->|\isasep\isanewline%
-\verb| ((string * cterm) list * cterm) * Proof.context| \\
+ \indexdef{}{ML}{Variable.focus}\verb|Variable.focus: term -> Proof.context ->|\isasep\isanewline%
+\verb| ((string * (string * typ)) list * term) * Proof.context| \\
\end{mldecls}
\begin{description}