--- a/thys/Lexer.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Lexer.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -15,7 +15,7 @@
 
 fun injval :: "rexp \<Rightarrow> char \<Rightarrow> val \<Rightarrow> val"
 where
-  "injval (CHAR d) c Void = Char d"
+  "injval (CH d) c Void = Char d"
 | "injval (ALT r1 r2) c (Left v1) = Left(injval r1 c v1)"
 | "injval (ALT r1 r2) c (Right v2) = Right(injval r2 c v2)"
 | "injval (SEQ r1 r2) c (Seq v1 v2) = Seq (injval r1 c v1) v2"
@@ -99,22 +99,22 @@
   then have "False" by cases
   then show "(c # s) \<in> ONE \<rightarrow> (injval ONE c v)" by simp
 next 
-  case (CHAR d)
+  case (CH d)
   consider (eq) "c = d" | (ineq) "c \<noteq> d" by blast
-  then show "(c # s) \<in> (CHAR d) \<rightarrow> (injval (CHAR d) c v)"
+  then show "(c # s) \<in> (CH d) \<rightarrow> (injval (CH d) c v)"
   proof (cases)
     case eq
-    have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+    have "s \<in> der c (CH d) \<rightarrow> v" by fact
     then have "s \<in> ONE \<rightarrow> v" using eq by simp
     then have eqs: "s = [] \<and> v = Void" by cases simp
-    show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" using eq eqs 
+    show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" using eq eqs 
     by (auto intro: Posix.intros)
   next
     case ineq
-    have "s \<in> der c (CHAR d) \<rightarrow> v" by fact
+    have "s \<in> der c (CH d) \<rightarrow> v" by fact
     then have "s \<in> ZERO \<rightarrow> v" using ineq by simp
     then have "False" by cases
-    then show "(c # s) \<in> CHAR d \<rightarrow> injval (CHAR d) c v" by simp
+    then show "(c # s) \<in> CH d \<rightarrow> injval (CH d) c v" by simp
   qed
 next
   case (ALT r1 r2)