diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/ListOrder.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -49,11 +49,11 @@
     "Ge == {(x,y). y <= x}"
 
 abbreviation
-  pfixLe :: "[nat list, nat list] => bool"  (infixl "pfixLe" 50)  where
+  pfixLe :: "[nat list, nat list] => bool"  (infixl \<open>pfixLe\<close> 50)  where
   "xs pfixLe ys == (xs,ys) \<in> genPrefix Le"
 
 abbreviation
-  pfixGe :: "[nat list, nat list] => bool"  (infixl "pfixGe" 50)  where
+  pfixGe :: "[nat list, nat list] => bool"  (infixl \<open>pfixGe\<close> 50)  where
   "xs pfixGe ys == (xs,ys) \<in> genPrefix Ge"