diff -r 8bb064045b4e -r e51c9a67a68d thys/Positions.thy
--- a/thys/Positions.thy	Thu Feb 25 22:46:58 2021 +0000
+++ b/thys/Positions.thy	Sun Oct 10 00:56:47 2021 +0100
@@ -527,8 +527,8 @@
   then show "Void :\<sqsubseteq>val v"
     by (simp add: PosOrd_ex_eq_def)
 next
-  case (Posix_CHAR c v)
-  have "v \<in> LV (CHAR c) [c]" by fact
+  case (Posix_CH c v)
+  have "v \<in> LV (CH c) [c]" by fact
   then have "v = Char c"
     by (simp add: LV_simps)
   then show "Char c :\<sqsubseteq>val v"