diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Nominal/Examples/Class2.thy
--- a/src/HOL/Nominal/Examples/Class2.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nominal/Examples/Class2.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -2949,12 +2949,12 @@
 done
 
 abbreviation
-  CANDn::"ty \<Rightarrow> ntrm set"  ("\<parallel>'(_')\<parallel>" [60] 60) 
+  CANDn::"ty \<Rightarrow> ntrm set"  (\<open>\<parallel>'(_')\<parallel>\<close> [60] 60) 
 where
   "\<parallel>(B)\<parallel> \<equiv> lfp (NEGn B \<circ> NEGc B)" 
 
 abbreviation
-  CANDc::"ty \<Rightarrow> ctrm set"  ("\<parallel><_>\<parallel>" [60] 60)
+  CANDc::"ty \<Rightarrow> ctrm set"  (\<open>\<parallel><_>\<parallel>\<close> [60] 60)
 where
   "\<parallel><B>\<parallel> \<equiv> NEGc B (\<parallel>(B)\<parallel>)"