diff -r 8b0b414e71b0 -r 3b8e3a156200 thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Wed Feb 20 00:00:30 2019 +0000
+++ b/thys/Sulzmann.thy	Sat Feb 23 21:52:06 2019 +0000
@@ -247,6 +247,12 @@
   shows "bmkeps r = retrieve r (mkeps (erase r))"
   using assms
   apply(induct r)
+       apply(simp)
+      apply(simp)
+     apply(simp)
+    apply(simp) 
+   apply(simp only: bmkeps.simps bnullable_correctness)
+  apply(auto simp only: split: if_split)
   apply(auto simp add: bnullable_correctness)
   done