--- a/thys/Simplifying.thy	Mon Mar 14 23:08:58 2016 +0000
+++ b/thys/Simplifying.thy	Tue Mar 15 01:10:38 2016 +0000
@@ -288,7 +288,7 @@
 apply(blast)
 prefer 2
 apply(auto)[1]
-apply (metis L_fst_simp Posix_elims(2) lex_correct3a)
+apply (metis L_fst_simp Posix_elims(2) lexer_correct_Some)
 apply(subst Posix_simp_nullable)
 using Posix.intros(1) Posix1(1) nullable_correctness apply blast
 apply(simp)
@@ -313,9 +313,9 @@
 apply(simp)
 apply(simp)
 apply(auto split: option.split prod.split)
-apply (metis L_fst_simp fst_conv lex_correct1a)
-using L_fst_simp lex_correct1a apply fastforce
-by (metis Posix_determ Posix_simp fst_conv lex_correct1 lex_correct3a option.distinct(1) option.inject snd_conv)
+apply (metis L_fst_simp fst_conv lexer_correct_None)
+using L_fst_simp lexer_correct_None apply fastforce
+by (metis Posix_determ Posix_simp fst_conv lexer_correct_None lexer_correct_Some option.distinct(1) option.inject snd_conv)