diff -r 27ea2ba48fa3 -r 6d8b29c7a960 doc-src/IsarImplementation/Thy/document/proof.tex
--- a/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Aug 31 22:55:49 2006 +0200
+++ b/doc-src/IsarImplementation/Thy/document/proof.tex	Thu Aug 31 23:01:16 2006 +0200
@@ -23,7 +23,7 @@
 }
 \isamarkuptrue%
 %
-\isamarkupsection{Local variables%
+\isamarkupsection{Variables and schematic polymorphism%
 }
 \isamarkuptrue%
 %
@@ -101,15 +101,6 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Schematic polymorphism%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-FIXME%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
 \isamarkupsection{Assumptions%
 }
 \isamarkuptrue%
@@ -128,7 +119,7 @@
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
-\isamarkupsection{Structured proofs \label{sec:isar-proof-state}%
+\isamarkupsection{Proof states \label{sec:isar-proof-state}%
 }
 \isamarkuptrue%
 %