--- a/Myhill.thy	Mon Jan 31 14:51:47 2011 +0000
+++ b/Myhill.thy	Wed Feb 02 06:05:12 2011 +0000
@@ -630,7 +630,7 @@
         *}
       case True
       with tag_xy have "y = []" 
-        by (auto simp:tag_str_STAR_def strict_prefix_def)
+        by (auto simp add: tag_str_STAR_def strict_prefix_def)
       thus ?thesis using xz_in_star True by simp
     next
         -- {* The nontrival case:
@@ -751,8 +751,7 @@
         -- {* 
            @{text "?thesis"} can easily be shown using properties of @{text "za"} and @{text "zb"}:
             *}
-        from step [OF l_za ls_zb]
-        have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" .
+        have "((y - ya) @ za) @ zb \<in> L\<^isub>1\<star>" using  l_za ls_zb by blast
         with eq_zab show ?thesis by simp
       qed
       with h5 h6 show ?thesis 
@@ -862,7 +861,8 @@
           using a_in by (auto elim:prefixE)        
         from x_za h7 have "(y - ya) @ za \<in> L\<^isub>1" 
           by (auto simp:str_eq_def str_eq_rel_def)
-        with z_decom b_in show ?thesis by (auto dest!:step[of "(y - ya) @ za"])
+	with b_in have "((y - ya) @ za) @ b \<in> L\<^isub>1\<star>" by blast
+        with z_decom show ?thesis by auto 
       qed
       with h5 h6 show ?thesis 
         by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
@@ -898,6 +898,7 @@
   shows "finite (UNIV // \<approx>(L r))"
 by (induct r) (auto)
 
+
 end
 
 (*