diff -r 454ced557605 -r 692911c0b981 thys3/src/BlexerSimp.thy
--- a/thys3/src/BlexerSimp.thy	Thu Jul 21 20:21:52 2022 +0100
+++ b/thys3/src/BlexerSimp.thy	Thu Jul 21 20:22:35 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: