# HG changeset patch
# User wenzelm
# Date 1249151674 -7200
# Node ID aa48c2b8f8e023b5334758bbe885b3ed5dc8f66d
# Parent  2b64fbc54a828743576c5cba50394f824bd311fe
updated Variable.import;

diff -r 2b64fbc54a82 -r aa48c2b8f8e0 doc-src/IsarImplementation/Thy/Proof.thy
--- 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}
 
diff -r 2b64fbc54a82 -r aa48c2b8f8e0 doc-src/IsarImplementation/Thy/document/Proof.tex
--- 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}