--- a/Myhill_2.thy	Sun Feb 20 11:14:07 2011 +0000
+++ b/Myhill_2.thy	Sun Feb 20 12:51:04 2011 +0000
@@ -481,7 +481,7 @@
 definition 
   tag_str_STAR :: "lang \<Rightarrow> string \<Rightarrow> lang set"
 where
-  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - xa} | xa. xa < x \<and> xa \<in> L1\<star>})"
+  "tag_str_STAR L1 \<equiv> (\<lambda>x. {\<approx>L1 `` {x - x'} | x'. x' < x \<and> x' \<in> L1\<star>})"
 
 text {* A technical lemma. *}
 lemma finite_set_has_max: "\<lbrakk>finite A; A \<noteq> {}\<rbrakk> \<Longrightarrow>