--- a/Myhill_2.thy	Sun Feb 20 07:33:54 2011 +0000
+++ b/Myhill_2.thy	Sun Feb 20 08:12:13 2011 +0000
@@ -302,7 +302,7 @@
   tag_str_SEQ :: "lang \<Rightarrow> lang \<Rightarrow> string \<Rightarrow> (lang \<times> lang set)"
 where
   "tag_str_SEQ L1 L2 \<equiv>
-     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - xa}) | xa.  xa \<le> x \<and> xa \<in> L1}))"
+     (\<lambda>x. (\<approx>L1 `` {x}, {(\<approx>L2 `` {x - x'}) | x'.  x' \<le> x \<and> x' \<in> L1}))"
 
 text {* The following is a techical lemma which helps to split the @{text "x @ z \<in> L\<^isub>1 ;; L\<^isub>2"} mentioned above.*}