--- a/thys/BitCoded.thy	Tue Jul 05 00:42:06 2022 +0100
+++ b/thys/BitCoded.thy	Sat Jul 09 14:11:07 2022 +0100
@@ -29,7 +29,7 @@
 where
   "decode' ds ZERO = (Void, [])"
 | "decode' ds ONE = (Void, ds)"
-| "decode' ds (CHAR d) = (Char d, ds)"
+| "decode' ds (CH d) = (Char d, ds)"
 | "decode' [] (ALT r1 r2) = (Void, [])"
 | "decode' (Z # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r1 in (Left v, ds'))"
 | "decode' (S # ds) (ALT r1 r2) = (let (v, ds') = decode' ds r2 in (Right v, ds'))"
@@ -111,7 +111,7 @@
 where
   "erase AZERO = ZERO"
 | "erase (AONE _) = ONE"
-| "erase (ACHAR _ c) = CHAR c"
+| "erase (ACHAR _ c) = CH c"
 | "erase (AALTs _ []) = ZERO"
 | "erase (AALTs _ [r]) = (erase r)"
 | "erase (AALTs bs (r#rs)) = ALT (erase r) (erase (AALTs bs rs))"
@@ -165,7 +165,7 @@
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
 | "intern ONE = AONE []"
-| "intern (CHAR c) = ACHAR [] c"
+| "intern (CH c) = ACHAR [] c"
 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
                                 (fuse [S]  (intern r2))"
 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"