diff -r d73f19be3ce6 -r 46e5566ad4ba thys/BitCodedCT.thy
--- a/thys/BitCodedCT.thy	Sat Jan 29 16:43:51 2022 +0000
+++ b/thys/BitCodedCT.thy	Sat Jan 29 23:53:21 2022 +0000
@@ -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'))"