diff -r 079fe4292526 -r c7723cc15de8 src/HOL/Analysis/Interval_Integral.thy
--- a/src/HOL/Analysis/Interval_Integral.thy	Sun Aug 25 20:54:20 2024 +0200
+++ b/src/HOL/Analysis/Interval_Integral.thy	Sun Aug 25 21:10:01 2024 +0200
@@ -148,6 +148,9 @@
   "_ascii_interval_lebesgue_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real measure \<Rightarrow> real \<Rightarrow> real"
   ("(5LINT _=_.._|_. _)" [0,60,60,61,100] 60)
 
+syntax_consts
+  "_ascii_interval_lebesgue_integral" == interval_lebesgue_integral
+
 translations
   "LINT x=a..b|M. f" == "CONST interval_lebesgue_integral M a b (\<lambda>x. f)"
 
@@ -159,6 +162,9 @@
   "_ascii_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real \<Rightarrow> real"
   ("(4LBINT _=_.._. _)" [0,60,60,61] 60)
 
+syntax_consts
+  "_ascii_interval_lebesgue_borel_integral" == interval_lebesgue_integral
+
 translations
   "LBINT x=a..b. f" == "CONST interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"
 
@@ -1045,11 +1051,17 @@
 syntax "_complex_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real \<Rightarrow> complex"
   ("(2CLBINT _. _)" [0,60] 60)
 
+syntax_consts
+  "_complex_lebesgue_borel_integral" == complex_lebesgue_integral
+
 translations "CLBINT x. f" == "CONST complex_lebesgue_integral CONST lborel (\<lambda>x. f)"
 
 syntax "_complex_set_lebesgue_borel_integral" :: "pttrn \<Rightarrow> real set \<Rightarrow> real \<Rightarrow> complex"
   ("(3CLBINT _:_. _)" [0,60,61] 60)
 
+syntax_consts
+  "_complex_set_lebesgue_borel_integral" == complex_set_lebesgue_integral
+
 translations
   "CLBINT x:A. f" == "CONST complex_set_lebesgue_integral CONST lborel A (\<lambda>x. f)"
 
@@ -1065,6 +1077,9 @@
   "_ascii_complex_interval_lebesgue_borel_integral" :: "pttrn \<Rightarrow> ereal \<Rightarrow> ereal \<Rightarrow> real \<Rightarrow> complex"
   ("(4CLBINT _=_.._. _)" [0,60,60,61] 60)
 
+syntax_consts
+  "_ascii_complex_interval_lebesgue_borel_integral" == complex_interval_lebesgue_integral
+
 translations
   "CLBINT x=a..b. f" == "CONST complex_interval_lebesgue_integral CONST lborel a b (\<lambda>x. f)"