diff -r 8bb064045b4e -r e51c9a67a68d thys/Sulzmann.thy
--- a/thys/Sulzmann.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Sulzmann.thy	Sun Oct 10 00:56:47 2021 +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'))"
@@ -88,7 +88,7 @@
 datatype arexp =
   AZERO
 | AONE "bit list"
-| ACHAR "bit list" char
+| ACH "bit list" char
 | ASEQ "bit list" arexp arexp
 | AALT "bit list" arexp arexp
 | ASTAR "bit list" arexp
@@ -96,7 +96,7 @@
 fun fuse :: "bit list \<Rightarrow> arexp \<Rightarrow> arexp" where
   "fuse bs AZERO = AZERO"
 | "fuse bs (AONE cs) = AONE (bs @ cs)" 
-| "fuse bs (ACHAR cs c) = ACHAR (bs @ cs) c"
+| "fuse bs (ACH cs c) = ACH (bs @ cs) c"
 | "fuse bs (AALT cs r1 r2) = AALT (bs @ cs) r1 r2"
 | "fuse bs (ASEQ cs r1 r2) = ASEQ (bs @ cs) r1 r2"
 | "fuse bs (ASTAR cs r) = ASTAR (bs @ cs) r"
@@ -104,7 +104,7 @@
 fun intern :: "rexp \<Rightarrow> arexp" where
   "intern ZERO = AZERO"
 | "intern ONE = AONE []"
-| "intern (CHAR c) = ACHAR [] c"
+| "intern (CH c) = ACH [] c"
 | "intern (ALT r1 r2) = AALT [] (fuse [Z] (intern r1)) 
                                 (fuse [S]  (intern r2))"
 | "intern (SEQ r1 r2) = ASEQ [] (intern r1) (intern r2)"
@@ -113,7 +113,7 @@
 
 fun retrieve :: "arexp \<Rightarrow> val \<Rightarrow> bit list" where
   "retrieve (AONE bs) Void = bs"
-| "retrieve (ACHAR bs c) (Char d) = bs"
+| "retrieve (ACH bs c) (Char d) = bs"
 | "retrieve (AALT bs r1 r2) (Left v) = bs @ retrieve r1 v"
 | "retrieve (AALT bs r1 r2) (Right v) = bs @ retrieve r2 v"
 | "retrieve (ASEQ bs r1 r2) (Seq v1 v2) = bs @ retrieve r1 v1 @ retrieve r2 v2"
@@ -126,7 +126,7 @@
 where
   "erase AZERO = ZERO"
 | "erase (AONE _) = ONE"
-| "erase (ACHAR _ c) = CHAR c"
+| "erase (ACH _ c) = CH c"
 | "erase (AALT _ r1 r2) = ALT (erase r1) (erase r2)"
 | "erase (ASEQ _ r1 r2) = SEQ (erase r1) (erase r2)"
 | "erase (ASTAR _ r) = STAR (erase r)"
@@ -136,7 +136,7 @@
 where
   "bnullable (AZERO) = False"
 | "bnullable (AONE bs) = True"
-| "bnullable (ACHAR bs c) = False"
+| "bnullable (ACH bs c) = False"
 | "bnullable (AALT bs r1 r2) = (bnullable r1 \<or> bnullable r2)"
 | "bnullable (ASEQ bs r1 r2) = (bnullable r1 \<and> bnullable r2)"
 | "bnullable (ASTAR bs r) = True"
@@ -155,7 +155,7 @@
 where
   "bder c (AZERO) = AZERO"
 | "bder c (AONE bs) = AZERO"
-| "bder c (ACHAR bs d) = (if c = d then AONE bs else AZERO)"
+| "bder c (ACH bs d) = (if c = d then AONE bs else AZERO)"
 | "bder c (AALT bs r1 r2) = AALT bs (bder c r1) (bder c r2)"
 | "bder c (ASEQ bs r1 r2) = 
      (if bnullable r1