--- a/Paper/Paper.thy	Wed Mar 24 12:34:28 2010 +0100
+++ b/Paper/Paper.thy	Wed Mar 24 12:53:39 2010 +0100
@@ -740,9 +740,9 @@
   functions. There are two kinds: free-variable functions corresponding to types,
   written $\fv\_ty$, and  free-variable functions corresponding to binding functions,
   written $\fv\_bn$. They have to be defined at the same time since there can
-  be interdependencies. Given a term-constructor $C ty_1 \ldots ty_n$ and some binding
-  clauses, the function $\fv (C x_1 \ldots x_n)$ will be the union of the values 
-  generated for each argument, say $x_i$, as follows:
+  be interdependencies. Given a term-constructor $C\_raw\;ty_1 \ldots ty_n$ and some 
+  binding clauses, the function $\fv (C\_raw\;x_1 \ldots x_n)$ will be the union 
+  of the values generated for each argument, say $x_i$, as follows:
 
   \begin{center}
   \begin{tabular}{cp{8cm}}