diff -r 91647a8d84a3 -r cdc0bdcfba3f thys/ReStar.thy
--- a/thys/ReStar.thy	Sun May 08 09:49:21 2016 +0100
+++ b/thys/ReStar.thy	Mon May 09 12:09:56 2016 +0100
@@ -170,8 +170,6 @@
 | Left val
 | Stars "val list"
 
-datatype_compat val
-
 
 section {* The string behind a value *}
 
@@ -215,9 +213,8 @@
 lemma Prf_flat_L:
   assumes "\<turnstile> v : r" shows "flat v \<in> L r"
 using assms
-apply(induct v r rule: Prf.induct)
-apply(auto simp add: Sequ_def)
-done
+by(induct v r rule: Prf.induct)
+  (auto simp add: Sequ_def)
 
 lemma Prf_Stars:
   assumes "\<forall>v \<in> set vs. \<turnstile> v : r"
@@ -457,8 +454,7 @@
 qed
 
 
-(* a proof that does not need proj *)
-lemma Posix2_roy_version:
+lemma Posix_injval:
   assumes "s \<in> (der c r) \<rightarrow> v"
   shows "(c # s) \<in> r \<rightarrow> (injval r c v)"
 using assms
@@ -636,7 +632,7 @@
 apply(drule_tac x="der a r" in meta_spec)
 apply(simp add: der_correctness Der_def)
 apply(rule iffI)
-apply(auto intro: Posix2_roy_version simp add: Posix1(1))
+apply(auto intro: Posix_injval simp add: Posix1(1))
 done