--- a/Paper/Paper.thy	Wed Jan 30 23:00:09 2013 +0000
+++ b/Paper/Paper.thy	Wed Jan 30 23:57:33 2013 +0000
@@ -891,7 +891,7 @@
   "tcopy_begin"}. Given the invariants @{term "inv_begin0"},\ldots,
   @{term "inv_begin4"} shown in Figure~\ref{invbegin} corresponding to 
   each state of @{term tcopy_begin}, we define the
-  following invariant for the whole program:
+  following invariant for the whole @{term tcopy_begin} program:
 
   \begin{figure}
   \begin{center}