diff -r 990c12ab1562 -r ea2e5acbfe4a Myhill_2.thy
--- a/Myhill_2.thy	Wed May 04 07:05:59 2011 +0000
+++ b/Myhill_2.thy	Mon May 09 07:25:37 2011 +0000
@@ -661,7 +661,7 @@
         with eq_zab show ?thesis by simp
       qed
       with h5 h6 show ?thesis 
-        by (drule_tac star_intro1, auto simp:strict_prefix_def elim:prefixE)
+        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
     qed
   } 
   -- {* By instantiating the reasoning pattern just derived for both directions:*} 
@@ -770,7 +770,7 @@
         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)
+        by (drule_tac star_intro1) (auto simp:strict_prefix_def elim:prefixE)
     qed
   } 
   -- {* By instantiating the reasoning pattern just derived for both directions:*}