--- a/Myhill_2.thy	Thu Jul 28 14:22:10 2011 +0000
+++ b/Myhill_2.thy	Thu Jul 28 17:52:36 2011 +0000
@@ -399,7 +399,7 @@
         proof -
           from h1 have "(x - xa_max) @ z \<noteq> []" 
             by (auto simp:strict_prefix_def elim:prefixE)
-          from star_decom [OF h3 this]
+	  from star_decom [OF h3 this]
           obtain a b where a_in: "a \<in> L\<^isub>1" 
             and a_neq: "a \<noteq> []" and b_in: "b \<in> L\<^isub>1\<star>" 
             and ab_max: "(x - xa_max) @ z = a @ b" by blast