--- a/Paper/Paper.thy	Tue Mar 30 13:23:12 2010 +0200
+++ b/Paper/Paper.thy	Tue Mar 30 13:36:02 2010 +0200
@@ -1238,7 +1238,7 @@
      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>\<^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>j"} has
+  $\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"}\\