--- a/Paper/Paper.thy	Tue Mar 23 13:03:42 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 13:07:02 2010 +0100
@@ -527,7 +527,8 @@
   collection of (possibly mutual recursive) type declarations, say
   $ty_{\alpha{}1}$, $ty_{\alpha{}2}$, \ldots $ty_{\alpha{}n}$, and a
   collection of associated binding function declarations, say
-  $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are written as follows:
+  $bn_{\alpha{}1}$, \ldots $bn_{\alpha{}m}$. They are schematically 
+  written as follows:
 
   \begin{center}
   \begin{tabular}{@ {\hspace{-9mm}}p{1.8cm}l}