--- a/thys/ReStar.thy	Sat Feb 13 02:00:09 2016 +0000
+++ b/thys/ReStar.thy	Mon Feb 15 21:48:57 2016 +0100
@@ -1456,17 +1456,8 @@
 apply metis
 apply metis
 apply(auto)[1]
-apply(simp add: L_flat_NPrf)
+apply(simp add: der_correctness Der_def)
 apply(auto)[1]
-apply(frule_tac c="c" in v3_proj)
-apply metis
-apply(drule_tac x="s\<^sub>3" in spec)
-apply(drule mp)
-apply(rule_tac x="projval r1 c v" in exI)
-apply(rule conjI)
-apply (metis v4_proj2)
-apply (metis NPrf_imp_Prf)
-apply metis
 (* nullable case *)
 apply(erule PMatch.cases)
 apply(simp_all)[7]