diff -r bb6732e135b2 -r 119b9f7e34c0 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 18:33:15 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 19:57:17 2011 +0200
@@ -442,7 +442,7 @@
   version of @{text "F\<^isub>C"} we made a modification by separating the
   grammars for type kinds and coercion kinds, as well as for types and coercion
   types. For this paper the interesting term-constructor is @{text "\<CASE>"},
-  which binds multiple type-, coercion- and term-variables.\label{corehas}}
+  which binds multiple type-, coercion- and term-variables (the overlines stand for lists).\label{corehas}}
   \end{figure}
 *}
 
@@ -2630,7 +2630,7 @@
 
   There are some restrictions we imposed in this paper that we would like to lift in
   future work. One is the exclusion of nested datatype definitions. Nested
-  datatype definitions allow one to specify, for instance, the function kinds
+  datatype definitions would allow one to specify, for instance, the function kinds
   in Core-Haskell as @{text "TFun string (ty list)"} instead of the unfolded
   version @{text "TFun string ty_list"} (see Figure~\ref{nominalcorehas}). To
   achieve this, we need more clever implementation than we have 
@@ -2662,8 +2662,8 @@
   informal notes \cite{SewellBestiary} available to us and also for patiently
   explaining some of the finer points of the Ott-tool.  Stephanie Weirich
   suggested to separate the subgrammars of kinds and types in our Core-Haskell
-  example. Ramana Kumar helped us with comments about an earlier version of 
-  this paper.
+  example. Ramana Kumar and Andrei Popescu helped us with comments about 
+  an earlier version of this paper.
 *}