diff -r 05843094273e -r 1cd509cba23f Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 17:52:16 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 17:55:46 2010 +0200
@@ -955,8 +955,8 @@
   \begin{center}
   \begin{tabular}{ll}
   @{text "Foo x::name y::name t::lam"} &  
-                              \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
-                              \isacommand{bind} @{text y} \isacommand{in} @{text t}  
+      \isacommand{bind} @{text x} \isacommand{in} @{text t},\;
+      \isacommand{bind} @{text y} \isacommand{in} @{text t}  
   \end{tabular}
   \end{center}
 
@@ -1004,12 +1004,12 @@
 
   As will shortly become clear, we cannot return an atom in a binding function
   that is also bound in the corresponding term-constructor. That means in the
-  example above that the term-constructors PVar and PTup must not have a
+  example above that the term-constructors @{text PVar} and @{text PTup} must not have a
   binding clause.  In the present version of Nominal Isabelle, we also adopted
   the restriction from the Ott-tool that binding functions can only return:
-  the empty set or empty list (as in case PNil), a singleton set or singleton
-  list containing an atom (case PVar), or unions of atom sets or appended atom
-  lists (case PTup). This restriction will simplify proofs later on.
+  the empty set or empty list (as in case @{text PNil}), a singleton set or singleton
+  list containing an atom (case @{text PVar}), or unions of atom sets or appended atom
+  lists (case @{text PTup}). This restriction will simplify proofs later on.
   
   The most drastic restriction we have to impose on deep binders is that 
   we cannot have ``overlapping'' deep binders. Consider for example the 
@@ -1097,10 +1097,10 @@
   given by user. In our implementation we just use an affix @{text "_raw"}.
   For the purpose of the paper we just use superscripts to indicate a
   notion defined over alpha-equivalence classes and leave out the superscript
-  for the corresponding notion on the ``raw'' level. So for example:
+  for the corresponding notion on the ``raw'' level. So for example we have
 
   \begin{center}
-  @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{7mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
+  @{text "ty\<^sup>\<alpha> \<mapsto> ty"} \hspace{2mm}and\hspace{2mm} @{text "C\<^sup>\<alpha> \<mapsto> C"}
   \end{center}
   
   \noindent
@@ -1123,20 +1123,20 @@
   %the @{text "ty"}s.
 
   The first non-trivial step we have to perform is the generation free-variable 
-  functions from the specifications. Given types @{text "ty\<^isub>1, \<dots>, ty\<^isub>n"}
-  we need to define the free-variable functions
+  functions from the specifications. Given the raw types @{text "ty\<^isub>1 \<dots> ty\<^isub>n"}
+  we need to define free-variable functions
 
   \begin{center}
-  @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
+  @{text "fv_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set    \<dots>    fv_ty\<^isub>n :: ty\<^isub>n \<Rightarrow> atom set"}
   \end{center}
 
   \noindent
   We define them together with the auxiliary free variable functions for
-  binding functions. Given binding functions of types
-  @{text "bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> \<dots> \<dots> bn\<^isub>m :: ty\<^isub>i\<^isub>m \<Rightarrow> \<dots>"} we need to define
+  binding functions. Given binding functions for raw types
+  @{text "bn_ty\<^isub>1 \<dots> bn_ty\<^isub>m"} we need to define
 
   \begin{center}
-  @{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"}
+  @{text "fv_bn_ty\<^isub>1 :: ty\<^isub>1 \<Rightarrow> atom set \<dots> fv_bn_ty\<^isub>m :: ty\<^isub>m \<Rightarrow> atom set"}
   \end{center}
 
   \noindent
@@ -1144,31 +1144,33 @@
   that are not bound in a term constructor, but because of the rather
   complicated binding mechanisms the details are somewhat involved. 
 
-  Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of type @{text ty} together with 
-  some  binding clauses, the function @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be 
-  the union of the values defined below for each argument, say @{text "x\<^isub>i"} with type @{text "ty\<^isub>i"}. 
-  From the binding clause of this term constructor, we can determine whether the 
-  argument @{text "x\<^isub>i"} is a shallow or deep binder, and in the latter case also 
-  whether it is a recursive or non-recursive of a binder. In these cases the value is: 
+  Given a term-constructor @{text "C"} of type @{text ty} with argument types
+  @{text "ty\<^isub>1 \<dots> ty\<^isub>n"} and some binding clauses, the function
+  @{text "fv_ty (C x\<^isub>1 \<dots> x\<^isub>n)"} will be the union of the values
+  defined below for each argument. From the binding clause of this term
+  constructor, we can determine whether the argument is a shallow or deep
+  binder, and in the latter case also whether it is a recursive or
+  non-recursive binder. In case the argument, say @{text "x\<^isub>i"} with
+  type @{text "ty\<^isub>i"}, is a binder, the value is:
 
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{term "{}"} provided @{text "x\<^isub>i"} is a shallow 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"}
+  $\bullet$ & @{text "fv_bn_ty\<^isub>i x\<^isub>i"} provided @{text "x\<^isub>i"} is a deep
+      non-recursive binder with the auxiliary function @{text "bn_ty\<^isub>i"}\\
+  $\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 with the auxiliary function @{text "bn_ty\<^isub>i"}
   \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. Let @{text "bnds"} be the bound atoms computed
+  one or more abstractions. Let @{text "bnds"} be the set of bound atoms calculated
   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
+  later case we just take the set of atoms specified binding
   function returns. With @{text "bnds"} computed as above the value of
   for @{text "x\<^isub>i"} is given by:
 
@@ -1177,17 +1179,18 @@
   $\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>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_ty\<^isub>i 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>i"}\\
 %  $\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}
 
-  \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
+  \noindent 
+  Next, for each binding function @{text "bn_ty"} we define a
+  free variable function @{text "fv_bn_ty"}. The basic idea behind this
+  function is to compute all the free atoms that are not bound by the 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"}.