diff -r 7a579f5533f8 -r 5af61c89f51e thys3/src/BlexerSimp.thy
--- a/thys3/src/BlexerSimp.thy	Sat Jul 16 18:34:46 2022 +0100
+++ b/thys3/src/BlexerSimp.thy	Sun Jul 17 13:07:05 2022 +0100
@@ -106,8 +106,6 @@
   apply(induct r rule: bnullable.induct) 
         apply(auto)
   apply (metis append.assoc bmkeps_retrieve bmkeps_retrieve_AALTs bnullable.simps(4))  
-   apply(case_tac n)
-  apply(auto)
   done
 
 lemma bmkepss_fuse: