diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/UNITY/PPROD.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -15,7 +15,7 @@
     "PLam I F == \<Squnion>i \<in> I. lift i (F i)"
 
 syntax
-  "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"  ("(3plam _:_./ _)" 10)
+  "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"  (\<open>(3plam _:_./ _)\<close> 10)
 syntax_consts
   "_PLam" == PLam
 translations