diff -r 79fdaad6f36b -r a42524ca6fc4 thys3/src/Blexer2.thy
--- a/thys3/src/Blexer2.thy	Sun May 08 09:58:50 2022 +0100
+++ b/thys3/src/Blexer2.thy	Sun May 08 15:38:00 2022 +0100
@@ -212,7 +212,7 @@
 | "bder c (ASEQs bs [r1]) = fuse bs (bder c r1)" 
 | "bder c (ASEQs bs (r1#rs)) =
      (if bnullable r1
-      then AALT bs (ASEQs [] ((bder c r1) # rs)) (fuse (bmkeps r1) (bder c (ASEQs [] rs)))
+      then AALT bs (ASEQs [] ((bder c r1) # rs)) (bder c (ASEQs (bmkeps r1) rs))
       else ASEQs bs ((bder c r1) # rs))"
 | "bder c (ASTAR bs r) = ASEQ (bs @ [Z]) (bder c r) (ASTAR [] r)"
 
@@ -262,13 +262,13 @@
   apply(case_tac va)
    apply(simp_all add: erase_fuse bnullable_correctness)      
   apply(auto)
-    apply(simp_all add: erase_fuse bnullable_correctness erase_ASEQs)   
-  done
+   apply(simp_all add: erase_fuse bnullable_correctness erase_ASEQs)
+  by (metis erase_ASEQs) 
 
 lemma erase_bders [simp]:
   shows "erase (bders r s) = ders s (erase r)"
   apply(induct s arbitrary: r )
-  apply(simp_all)
+   apply(simp_all)
   done
 
 lemma bnullable_fuse: