--- a/thys/ReStar.thy	Wed Mar 02 14:06:13 2016 +0000
+++ b/thys/ReStar.thy	Wed Mar 02 14:35:50 2016 +0000
@@ -136,7 +136,7 @@
 where
   "der c (ZERO) = ZERO"
 | "der c (ONE) = ZERO"
-| "der c (CHAR c') = (if c = c' then ONE else ZERO)"
+| "der c (CHAR d) = (if c = d then ONE else ZERO)"
 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
 | "der c (SEQ r1 r2) = 
      (if nullable r1
@@ -399,7 +399,7 @@
 apply(erule Prf.cases)
 apply(simp_all)[7]
 apply(simp)
-apply(case_tac "c = c'")
+apply(case_tac "c = d")
 apply(simp)
 apply(auto)[1]
 apply(erule Prf.cases)
@@ -1168,7 +1168,7 @@
 apply(erule PMatch.cases)
 apply(simp_all)[7]
 (* CHAR case *)
-apply(case_tac "c = c'")
+apply(case_tac "c = d")
 apply(simp)
 apply(erule PMatch.cases)
 apply(simp_all)[7]