# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1652021044 -3600
# Node ID e97681d4edaea9a8bcb96580aa9e6f8e34eb1987
# Parent  a42524ca6fc4802d487035f4defc6bc06a242c3c# Parent  9db279e3ac55afc2ae25b5cb253cca9313d9e61b
updated

diff -r 9db279e3ac55 -r e97681d4edae thys3/src/Blexer2.thy
--- a/thys3/src/Blexer2.thy	Sun May 08 15:29:33 2022 +0100
+++ b/thys3/src/Blexer2.thy	Sun May 08 15:44:04 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: