diff -r f5ab2f02d148 -r 44914e2724b7 thys/BitCoded.thy
--- a/thys/BitCoded.thy	Mon Jul 29 21:39:46 2019 +0100
+++ b/thys/BitCoded.thy	Tue Jul 30 10:44:12 2019 +0100
@@ -2688,14 +2688,7 @@
     apply(simp)
   (* AALT case *)
    prefer 2
-  apply(simp only:)
-  (* *)
-  apply(simp)
-   apply(subst WWW5)
-  
-
-
-
+   apply(simp only:)
    apply(case_tac "\<exists>a1 a2. x52 = [a1, a2]")
     apply(clarify)
   apply(simp del: bsimp.simps)