--- a/doc-src/IsarImplementation/Thy/document/Proof.tex Mon Oct 25 11:39:52 2010 +0200
+++ b/doc-src/IsarImplementation/Thy/document/Proof.tex Mon Oct 25 16:14:40 2010 +0200
@@ -299,12 +299,12 @@
\endisadelimML
%
\begin{isamarkuptext}%
-In the above example, the starting context had been derived
- from the toplevel theory, which means that fixed variables are
- internalized literally: \verb|x| is mapped again to
- \verb|x|, and attempting to fix it again in the subsequent
- context is an error. Alternatively, fixed parameters can be renamed
- explicitly as follows:%
+In the above example, the starting context is derived from the
+ toplevel theory, which means that fixed variables are internalized
+ literally: \verb|x| is mapped again to \verb|x|, and
+ attempting to fix it again in the subsequent context is an error.
+ Alternatively, fixed parameters can be renamed explicitly as
+ follows:%
\end{isamarkuptext}%
\isamarkuptrue%
%