diff -r d688a01b8f89 -r 1a4e5b94293b thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Mon Sep 10 21:41:54 2018 +0100
+++ b/thys/Sulzmann.thy	Sun Sep 30 12:02:04 2018 +0100
@@ -312,9 +312,19 @@
   }
   then show "blexer r s = lexer r s"
     unfolding blexer_def lexer_flex
-    by(auto simp add: bnullable_correctness[symmetric])
+    apply(subst bnullable_correctness[symmetric])
+    apply(simp)
+    done
 qed
 
+fun simp where
+  "simp (AALT bs a AZERO) = fuse bs (simp a)"
+| "simp (AALT bs AZERO a) = fuse bs (simp a)"
+| "simp (ASEQ bs a AZERO) = AZERO"
+| "simp (ASEQ bs AZERO a) = AZERO"
+| "simp a = a"
+
+
 unused_thms
   
 end
\ No newline at end of file