diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Analysis/Bounded_Linear_Function.thy
--- a/src/HOL/Analysis/Bounded_Linear_Function.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Analysis/Bounded_Linear_Function.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -116,7 +116,7 @@
 
 subsection \<open>Type of bounded linear functions\<close>
 
-typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun ("(_ \<Rightarrow>\<^sub>L /_)" [22, 21] 21) =
+typedef\<^marker>\<open>tag important\<close> (overloaded) ('a, 'b) blinfun (\<open>(_ \<Rightarrow>\<^sub>L /_)\<close> [22, 21] 21) =
   "{f::'a::real_normed_vector\<Rightarrow>'b::real_normed_vector. bounded_linear f}"
   morphisms blinfun_apply Blinfun
   by (blast intro: bounded_linear_intros)
@@ -663,7 +663,7 @@
 lift_definition blinfun_compose::
   "'a::real_normed_vector \<Rightarrow>\<^sub>L 'b::real_normed_vector \<Rightarrow>
     'c::real_normed_vector \<Rightarrow>\<^sub>L 'a \<Rightarrow>
-    'c \<Rightarrow>\<^sub>L 'b" (infixl "o\<^sub>L" 55) is "(o)"
+    'c \<Rightarrow>\<^sub>L 'b" (infixl \<open>o\<^sub>L\<close> 55) is "(o)"
   parametric comp_transfer
   unfolding o_def
   by (rule bounded_linear_compose)