--- a/thys/Lexer.thy	Wed Aug 15 13:48:57 2018 +0100
+++ b/thys/Lexer.thy	Thu Aug 16 01:12:00 2018 +0100
@@ -290,18 +290,14 @@
 lemma flex_append:
   shows "flex r f (s1 @ s2) = flex (ders s1 r) (flex r f s1) s2"
   apply(induct s1 arbitrary: s2 r f)
-   apply(simp)
-  apply(drule_tac x="s2" in meta_spec)
-  apply(drule_tac x="der a r" in meta_spec)
-  apply(simp)
+  apply(simp_all)
   done  
 
 lemma lexer_flex:
   shows "lexer r s = (if nullable (ders s r) 
                       then Some(flex r id s (mkeps (ders s r))) else None)"
   apply(induct s arbitrary: r)
-  apply(simp)
-  apply(simp add: flex_fun_apply)
+  apply(simp_all add: flex_fun_apply)
   done  
 
 unused_thms