# HG changeset patch
# User wenzelm
# Date 1724619296 -7200
# Node ID fd01ef524169155964ce76d0af8d25172252017f
# Parent  c7723cc15de8c8d8e5341d06bb586d16c9d92913
use nicer notation, following 783406dd051e;

diff -r c7723cc15de8 -r fd01ef524169 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sun Aug 25 21:10:01 2024 +0200
+++ b/src/HOL/GCD.thy	Sun Aug 25 22:54:56 2024 +0200
@@ -2933,7 +2933,7 @@
 
 end
 
-lemma (in semiring_char_0) CHAR_eq_0 [simp]: "semiring_char TYPE('a) = 0"
+lemma (in semiring_char_0) CHAR_eq_0 [simp]: "CHAR('a) = 0"
   by (simp add: CHAR_eq0_iff)