--- a/thys/BitCoded2.thy	Wed Aug 21 10:29:34 2019 +0200
+++ b/thys/BitCoded2.thy	Thu Aug 22 01:11:07 2019 +0200
@@ -3621,18 +3621,7 @@
   apply(subgoal_tac "rsX \<noteq> []")
    prefer 2
    apply (metis arexp.distinct(7) good.simps(4) good1)
-  apply(subgoal_tac "\<exists>XX. XX \<in> set rsX")
-   prefer 2
-  using neq_Nil_conv apply fastforce
-  apply(erule exE)
-  apply(rule_tac x="fuse bsX XX" in bexI)
-   prefer 2
-   apply blast
-  apply(frule f_cont1)
-  apply(auto)
-  apply(rule contains0)
-  apply(drule contains49)
-  by (simp add: in2)
+  by (metis contains0 contains49 f_cont1 in2 list.exhaust list.set_intros(1))
 
 lemma CONTAINS1:
   assumes "a >> bs"
@@ -3800,6 +3789,7 @@
   assumes "r = AALTs [S] [ASEQ [S] (AALTs [S] [AONE [S], ACHAR [S] c]) (ACHAR [S] c)]"
   shows "bsimp r = XXX"
   and   "bder c r = XXX"
+  and   "bder c (bsimp r) = XXX"
   and   "bsimp (bder c (bsimp r)) = XXX"
   and   "bsimp (bder c r) = XXX"
   apply(simp_all add: assms)