diff -r 232aa2f19a75 -r ec5e4fe4cc70 thys/RegLangs.thy
--- a/thys/RegLangs.thy	Sun Oct 10 09:56:01 2021 +0100
+++ b/thys/RegLangs.thy	Sun Oct 10 18:35:21 2021 +0100
@@ -201,7 +201,7 @@
 datatype ctxt = 
     SeqC rexp bool
   | AltCL rexp
-  | AltCR rexp 
+  | AltCH rexp 
   | StarC rexp 
 
 function
@@ -215,13 +215,13 @@
      (if c = d then up c ONE ctxts else up c ZERO ctxts)"
 | "down c ONE ctxts = up c ZERO ctxts"
 | "down c ZERO ctxts = up c ZERO ctxts"
-| "down c (ALT r1 r2) ctxts = down c r1 (AltCR r2 # ctxts)"
+| "down c (ALT r1 r2) ctxts = down c r1 (AltCH r2 # ctxts)"
 | "down c (STAR r1) ctxts = down c r1 (StarC r1 # ctxts)"
 | "up c r [] = (r, [])"
 | "up c r (SeqC r2 False # ctxts) = up c (SEQ r r2) ctxts"
 | "up c r (SeqC r2 True # ctxts) = down c r2 (AltCL (SEQ r r2) # ctxts)"
 | "up c r (AltCL r1 # ctxts) = up c (ALT r1 r) ctxts"
-| "up c r (AltCR r2 # ctxts) = down c r2 (AltCL r # ctxts)"
+| "up c r (AltCH r2 # ctxts) = down c r2 (AltCL r # ctxts)"
 | "up c r (StarC r1 # ctxts) = up c (SEQ r (STAR r1)) ctxts"
   apply(pat_completeness)
   apply(auto)