diff -r 18d19d039ac9 -r f476c98cad28 thys/LexerExt.thy
--- a/thys/LexerExt.thy	Sat Mar 11 12:50:01 2017 +0000
+++ b/thys/LexerExt.thy	Sat Mar 11 19:33:38 2017 +0000
@@ -1159,12 +1159,12 @@
 next
   case (Posix_NMTIMES1 s1 r v s2 n m vs v2)
   have "(s1 @ s2) \<in> NMTIMES r (Suc n) (Suc m) \<rightarrow> v2" 
-       "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n m) \<rightarrow> Stars vs"
+       "s1 \<in> r \<rightarrow> v" "s2 \<in> (NMTIMES r n m) \<rightarrow> Stars vs" "flat v = [] \<Longrightarrow> flat (Stars vs) = []"
        "\<not> (\<exists>s\<^sub>3 s\<^sub>4. s\<^sub>3 \<noteq> [] \<and> s\<^sub>3 @ s\<^sub>4 = s2 \<and> s1 @ s\<^sub>3 \<in> L r \<and> s\<^sub>4 \<in> L (NMTIMES r n m))" by fact+
   then obtain v' vs' where "v2 = Stars (v' # vs')" "s1 \<in> r \<rightarrow> v'" "s2 \<in> (NMTIMES r n m) \<rightarrow> (Stars vs')"
   apply(cases) apply (auto simp add: append_eq_append_conv2)
   using Posix1(1) apply fastforce
-  by (m etis Posix1(1) Posix_NMTIMES1.hyps(5) append_Nil append_Nil2)
+  by (metis Posix1(1) Posix_NMTIMES1.hyps(6) self_append_conv self_append_conv2)
   moreover
   have IHs: "\<And>v2. s1 \<in> r \<rightarrow> v2 \<Longrightarrow> v = v2"
             "\<And>v2. s2 \<in> NMTIMES r n m \<rightarrow> v2 \<Longrightarrow> Stars vs = v2" by fact+
@@ -1569,6 +1569,8 @@
         apply(blast)
         apply(simp)
         apply(simp add: der_correctness Der_def)
+        using Posix1a Prf_injval_flat list.distinct(1) apply auto[1]
+        apply(simp add: der_correctness Der_def)
         done
 next 
   case (PLUS r)