diff -r ccd2ab0cebf3 -r 88b33de74e61 Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 30 12:19:20 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 12:31:28 2010 +0200
@@ -1185,10 +1185,10 @@
   @{text "\<approx>bn\<^isub>1 :: ty\<^isub>i\<^isub>1 \<Rightarrow> ty\<^isub>i\<^isub>1 \<Rightarrow> bool \<dots> \<approx>bn\<^isub>n :: ty\<^isub>i\<^isub>m \<Rightarrow> ty\<^isub>i\<^isub>m \<Rightarrow> bool"}
   \end{center}
 
-  Given a term-constructor @{text "C ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
-  of this constructor are alpha-equivalent @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if there
+  Given a term-constructor @{text "C_raw ty\<^isub>1 \<dots> ty\<^isub>n"}, of a type @{text ty}, two instances
+  of this constructor are alpha-equivalent @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if there
   exist permutations @{text "\<pi>\<^isub>1 \<dots> \<pi>\<^isub>p"} (one for each bound argument) such that
-  the conjunction of equivalences for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
+  the conjunction of equivalences defined below for each argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} holds.
   For an argument pair @{text "x\<^isub>j"}, @{text "y\<^isub>j"} this holds if:
 
   \begin{center}
@@ -1200,14 +1200,14 @@
      provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding
      function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound
      free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and
-     @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>n"}\\
+     @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\
   $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\
-  $\bullet$ & @{term "(x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>n"}
-     is bound in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the
+  $\bullet$ & @{term "({x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} has
+     a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
      alpha-equivalence for @{term "x\<^isub>j"}
      and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
-  $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided  @{text "bn\<^isub>m x\<^isub>n"}
-    is bound non-recursively in @{text "x\<^isub>j"} with permutation @{text "\<pi>"}, @{term "R"} is the
+  $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"}
+     has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the
      alpha-equivalence for @{term "x\<^isub>j"}
      and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\
   $\bullet$ & @{text "x\<^isub>j \<approx>\<^isub>j y\<^isub>j"} for a nominal datatype with no bindings (this includes
@@ -1220,8 +1220,8 @@
   for their respective types, the difference is that they ommit checking the arguments that
   are bound. We assumed that there are no bindings in the type on which the binding function
   is defined so, there are no permutations involved. For a binding function clause 
-  @{text "bn (C x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
-  @{text "C x\<^isub>1 \<dots> x\<^isub>n \<approx> C y\<^isub>1 \<dots> y\<^isub>n"} if:
+  @{text "bn (C_raw x\<^isub>1 \<dots> x\<^isub>n) = rhs"}, two instances of the constructor are equivalent
+  @{text "C_raw x\<^isub>1 \<dots> x\<^isub>n \<approx> C_raw y\<^isub>1 \<dots> y\<^isub>n"} if:
   \begin{center}
   \begin{tabular}{cp{7cm}}
   $\bullet$ & @{text "x\<^isub>j"} is not a nominal datatype and occurs in @{text "rhs"}\\