--- a/Nominal/ROOT.ML	Wed Mar 24 12:34:28 2010 +0100
+++ b/Nominal/ROOT.ML	Wed Mar 24 12:53:39 2010 +0100
@@ -14,7 +14,8 @@
     "ExLet",
     "ExLetRec",
     "ExTySch",
-    "ExLeroy"
+    "ExLeroy",
+    "Test"
 (*  "ExCoreHaskell", *)
 (*  "ExPS3", *)
 (*  "ExPS6", *)

--- a/Nominal/Test.thy	Wed Mar 24 12:34:28 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 24 12:53:39 2010 +0100
@@ -1,3 +1,4 @@
+(*<*)
 theory Test
 imports "Parser"
 begin
@@ -106,6 +107,6 @@
 (* run out of steam at the moment *)
 
 end
+(*>*)
 
 
-

--- 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}}