diff -r 57182b36ec01 -r 41a2a3b63853 thys2/SizeBound4.thy
--- a/thys2/SizeBound4.thy	Sun Feb 06 00:02:04 2022 +0000
+++ b/thys2/SizeBound4.thy	Mon Feb 07 01:11:25 2022 +0000
@@ -179,7 +179,7 @@
 | "bmkeps(ASEQ bs r1 r2) = bs @ (bmkeps r1) @ (bmkeps r2)"
 | "bmkeps(AALTs bs rs) = bs @ (bmkepss rs)"
 | "bmkeps(ASTAR bs r) = bs @ [S]"
-| "bmkepss [] = []"
+(*| "bmkepss [] = []"*)
 | "bmkepss (r # rs) = (if bnullable(r) then (bmkeps r) else (bmkepss rs))"
 
 lemma bmkepss1:
@@ -849,7 +849,7 @@
   have as1: "L(erase a2) \<subseteq> L(erase a1)" by fact
   have as3: "bnullables (rsa @ [a1] @ rsb @ [a2] @ rsc)" by fact
   show "bmkepss (rsa @ [a1] @ rsb @ [a2] @ rsc) = bmkepss (rsa @ [a1] @ rsb @ rsc)" using as1 as3
-    by (smt (verit, ccfv_SIG) append_Cons bmkepss.simps(2) bmkepss1 bmkepss2 bnullable_correctness nullable_correctness subset_eq)
+    by (smt (verit, ccfv_SIG) append_Cons bmkepss.simps(1) bmkepss1 bmkepss2 bnullable_correctness nullable_correctness subset_eq)
 (*next 
   case (extra bs0 bs1 r1 bs2 r2 bs4 bs3)
   then show ?case