--- a/Paper/Paper.thy	Tue Mar 30 11:45:41 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 12:19:20 2010 +0200
@@ -1122,26 +1122,27 @@
   \noindent
   In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
   one or more abstractions. Let @{text "bnds"} be the bound atoms computed
-  as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{text "{}"}.
+  as follows: If @{text "x\<^isub>i"} is not a body of an abstraction @{term "{}"}.
   Otherwise there are two cases: either the
   corresponding binders are all shallow or there is a single deep binder.
   In the former case we build the union of all shallow binders; in the
   later case we just take set or list of atoms the specified binding
   function returns. With @{text "bnds"} computed as above the value of
-  for @{text "x\<^isub>i"} is given by:  
- 
+  for @{text "x\<^isub>i"} is given by:
+
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{text "{atom x\<^isub>i} - bnds"} provided @{term "x\<^isub>i"} is an atom\\
   $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
   $\bullet$ & @{text "(atoms (set x\<^isub>i)) - bnds"} provided @{term "x\<^isub>i"} is a list of atoms\\
-  $\bullet$ & @{text "(fv_ty\<^isub>i x\<^isub>i) - bnds"} provided @{term "ty\<^isub>i"} is a nominal datatype\\
-  $\bullet$ & @{term "{}"} otherwise 
+  $\bullet$ & @{text "(fv_ty\<^isub>m x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is one of the datatypes
+     we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
+  $\bullet$ & @{text "(fv\<^isup>\<alpha> x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a defined nominal datatype
+     with a free variable function @{text "fv\<^isup>\<alpha>"}\\\\
+  $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
   \end{center}
 
-\marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?}
-
   \noindent Next, for each binding function @{text "bn"} we define a
   free variable function @{text "fv_bn"}. The basic idea behind this
   function is to compute all the free atoms under this binding
@@ -1153,18 +1154,19 @@
   we define @{text "fv_bn"} to be the union of the values calculated
   for @{text "x\<^isub>j"} as follows:
 
- \marginpar{raw for being defined}
-
   \begin{center}
   \begin{tabular}{cp{7cm}}
-  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\
+  $\bullet$ & @{term "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom,
+     atom list or atom set\\
   $\bullet$ & @{text "fv_bn\<^isub>m x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} 
     with the recursive call @{text "bn\<^isub>m x\<^isub>j"}\\
-  $\bullet$ & @{text "(atoms x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a set of atoms\\
-  $\bullet$ & @{text "(atoml x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a list of atoms\\
-  $\bullet$ & @{text "(fv_ty x\<^isub>j) - bnds"} provided @{term "x\<^isub>j"} is a nominal datatype
-    with a free variable function @{text "fv_ty"}. This includes the types being
-    defined, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\
+  $\bullet$ & @{text "atoms x\<^isub>j"} provided @{term "x\<^isub>j"} is a set of atoms not in @{text "rhs"}\\
+  $\bullet$ & @{term "atoml x\<^isub>j"} provided @{term "x\<^isub>j"} is a list of atoms not in @{text "rhs"}\\
+  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>j"} provided @{term "x\<^isub>j"} is not in @{text "rhs"} and is 
+     one of the datatypes
+     we are defining, with the free variable function @{text "fv_ty\<^isub>m"}\\
+  $\bullet$ & @{text "fv_ty\<^isup>\<alpha> x\<^isub>j - bnds"} provided @{term "x\<^isub>j"}  is not in @{text "rhs"}
+     and is an existing nominal datatype with the free variable function @{text "fv\<^isup>\<alpha>"}\\
   $\bullet$ & @{term "{}"} otherwise
   \end{tabular}
   \end{center}