# HG changeset patch
# User wenzelm
# Date 1304198877 -7200
# Node ID 9d107a52b6345eeb8f39f11ebafe6d3aa5bae4b3
# Parent  e21362bf1d93dd03134cbf092c0b68a116fa28cf
updated Variable.focus;

diff -r e21362bf1d93 -r 9d107a52b634 doc-src/IsarImplementation/Thy/Proof.thy
--- 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}
diff -r e21362bf1d93 -r 9d107a52b634 doc-src/IsarImplementation/Thy/document/Proof.tex
--- 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}