--- a/Paper/Paper.thy	Tue Mar 30 02:55:18 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 09:00:52 2010 +0200
@@ -1089,11 +1089,11 @@
   \end{center}
 
   \noindent
-  and given binding functions @{text "bn_ty\<^isub>1, \<dots>, bn_ty\<^isub>m"} we also need to define 
-  the free-variable functions
+  We define them together with the auxiliary free variable functions for
+  binding functions
 
   \begin{center}
-  @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
+  @{text "fv_bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> atom set"}
   \end{center}
 
   \noindent
@@ -1111,19 +1111,23 @@
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow binder\\
-  $\bullet$ & @{text "ft_bn_by\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep non-recursive binder\\
-  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep recursive binder\\
+  $\bullet$ & @{text "fv_bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+      non-recursive binder with the auxiliary function @{text "bn\<^isub>j"}\\
+  $\bullet$ & @{text "fv_ty\<^isub>i x\<^isub>i - bn\<^isub>j x\<^isub>i"} provided @{text "x\<^isub>i"} is
+      a deep recursive binder with the auxiliary function @{text "bn\<^isub>j"}
   \end{tabular}
   \end{center}
 
   \noindent
   In case the argument @{text "x\<^isub>i"} is not a binder, it might be a body of
-  one or more abstractions. 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 
+  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 "{}"}.
+  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. Let @{text "bnds"} be an abbreviation of the bound
-  atoms. Then the value is given by:  
+  function returns. With @{text "bnds"} computed as above the value of
+  for @{text "x\<^isub>i"} is given by:  
  
   \begin{center}
   \begin{tabular}{cp{7cm}}
@@ -1135,31 +1139,30 @@
   \end{tabular}
   \end{center}
 
-  \noindent
-  If the argument is neither a binder, nor a body of an abstraction, then the 
-  value is defined as above, except that @{text "bnds"} is empty. i.e.~no atoms
-  are abstracted.
+\marginpar{\small We really have @{text "bn_raw"}, @{text "fv_bn_raw"}. Should we mention this?}
 
-  TODO
 
-  Given a clause of a binding function of the form 
+  \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
+  function. So given that @{text "bn"} is a binding function for type
+  @{text "ty\<^isub>i"} it will be the same as @{text "fv_ty\<^isub>i"} with the
+  omission of the arguments present in @{text "bn"}.
 
-  \begin{center}
-  @{text "bn_ty (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}
-  \end{center}
-
-  \noindent
-  then the corresponding free-variable function @{text "fv_bn_ty\<^isub>i"} is the
-  union of the values calculated for the @{text "x\<^isub>j"} as follows:
+  For a binding function clause @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"},
+  we define @{text "fv_bn"} to be the union of the values calculated
+  for @{text "x\<^isub>j"} as follows:
 
   \begin{center}
   \begin{tabular}{cp{7cm}}
-  $\bullet$ & @{text "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\
-  $\bullet$ & @{text "fv_bn_ty x\<^isub>j"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} 
-    with the recursive call @{text "bn_ty x\<^isub>j"}\\
-  $\bullet$ & @{text "(atoms x\<^isub>i) - bnds"} provided @{term "x\<^isub>i"} is a set of atoms\\
-  $\bullet$ & @{text "(atoml 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 "{}"} provided @{term "x\<^isub>j"} occurs in @{text "rhs"} and is an atom\\
+  $\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 currently defined
+    types, where we use an appropriate @{term "fv_ty\<^isub>i"} function.\\
   $\bullet$ & @{term "{}"} otherwise 
   \end{tabular}
   \end{center}
@@ -1304,4 +1307,4 @@
 
 (*<*)
 end
-(*>*)
\ No newline at end of file
+(*>*)