--- a/thys/ReStar.thy	Sun Feb 28 14:01:12 2016 +0000
+++ b/thys/ReStar.thy	Tue Mar 01 12:10:11 2016 +0000
@@ -184,6 +184,9 @@
 | Left val
 | Stars "val list"
 
+datatype_compat val
+
+
 section {* The string behind a value *}
 
 fun 
@@ -352,7 +355,7 @@
 apply(erule Prf.cases)
 apply(simp_all)[7]
 (* CHAR *)
-apply(case_tac "c = char")
+apply(case_tac "c = x")
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[7]
@@ -361,7 +364,7 @@
 apply(erule Prf.cases)
 apply(simp_all)[7]
 (* SEQ *)
-apply(case_tac "nullable rexp1")
+apply(case_tac "nullable x1")
 apply(simp)
 apply(erule Prf.cases)
 apply(simp_all)[7]
@@ -491,10 +494,14 @@
 apply(metis PMatch.intros(7))
 done
 
+find_theorems Stars
+thm compat_val_list.induct compat_val.induct
+
+
 lemma PMatch_determ:
   shows "\<lbrakk>s \<in> r \<rightarrow> v1; s \<in> r \<rightarrow> v2\<rbrakk> \<Longrightarrow> v1 = v2"
   and   "\<lbrakk>s \<in> (STAR r) \<rightarrow> Stars vs1; s \<in> (STAR r) \<rightarrow> Stars vs2\<rbrakk> \<Longrightarrow> vs1 = vs2"
-apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: val.inducts)
+apply(induct v1 and vs1 arbitrary: s r v2 and s r vs2 rule: compat_val.induct compat_val_list.induct)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 apply(erule PMatch.cases)
@@ -604,7 +611,7 @@
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 (* CHAR case *)
-apply(case_tac "c = char")
+apply(case_tac "c = x")
 apply(simp)
 apply(erule PMatch.cases)
 apply(simp_all)[7]
@@ -622,7 +629,7 @@
 apply metis
 apply(simp add: der_correctness Der_def)
 (* SEQ case *)
-apply(case_tac "nullable rexp1")
+apply(case_tac "nullable x1")
 apply(simp)
 prefer 2
 (* not-nullbale case *)
@@ -997,7 +1004,7 @@
   shows "\<turnstile> v : r \<Longrightarrow> \<exists>v'. flat v' = flat v \<and> \<Turnstile> v' : r"
   and   "\<turnstile> Stars vs : r \<Longrightarrow> \<exists>vs'. flat (Stars vs') = flat (Stars vs) \<and> \<Turnstile> Stars vs' : r"
 using assms
-apply(induct v and vs arbitrary: r and r rule: val.inducts)
+apply(induct v and vs arbitrary: r and r rule: compat_val.induct compat_val_list.induct)
 apply(auto)[1]
 apply(erule Prf.cases)
 apply(simp_all)[7]