diff -r c007e6d9941d -r c92efbf32bfe src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Tue Oct 01 20:39:16 2024 +0200
+++ b/src/HOL/HOL.thy	Tue Oct 01 21:30:59 2024 +0200
@@ -191,11 +191,11 @@
 nonterminal case_syn and cases_syn
 syntax
   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  (\<open>(\<open>notation=\<open>mixfix case expression\<close>\<close>case _ of/ _)\<close> 10)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ \<Rightarrow>/ _)\<close> 10)
   "" :: "case_syn \<Rightarrow> cases_syn"  (\<open>_\<close>)
   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  (\<open>_/ | _\<close>)
 syntax (ASCII)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case pattern\<close>\<close>_ =>/ _)\<close> 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  (\<open>(\<open>indent=2 notation=\<open>mixfix case clause\<close>\<close>_ =>/ _)\<close> 10)
 
 notation (ASCII)
   All  (binder \<open>ALL \<close> 10) and