diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/Nominal/Examples/VC_Condition.thy
--- a/src/HOL/Nominal/Examples/VC_Condition.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/Nominal/Examples/VC_Condition.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -16,7 +16,7 @@
 nominal_datatype lam = 
     Var "name"
   | App "lam" "lam"
-  | Lam "\<guillemotleft>name\<guillemotright>lam" ("Lam [_]._" [100,100] 100)
+  | Lam "\<guillemotleft>name\<guillemotright>lam" (\<open>Lam [_]._\<close> [100,100] 100)
 
 text \<open>
   The inductive relation 'unbind' unbinds the top-most  
@@ -27,7 +27,7 @@
   of the algorithm W.\<close>
 
 inductive
-  unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" ("_ \<mapsto> _,_" [60,60,60] 60)
+  unbind :: "lam \<Rightarrow> name list \<Rightarrow> lam \<Rightarrow> bool" (\<open>_ \<mapsto> _,_\<close> [60,60,60] 60)
 where
   u_var: "(Var a) \<mapsto> [],(Var a)"
 | u_app: "(App t1 t2) \<mapsto> [],(App t1 t2)"
@@ -143,7 +143,7 @@
   strips off the top-most binders from lambdas.\<close>
 
 inductive
-  strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" ("_ \<rightarrow> _" [60,60] 60)
+  strip :: "lam \<Rightarrow> lam \<Rightarrow> bool" (\<open>_ \<rightarrow> _\<close> [60,60] 60)
 where
   s_var: "(Var a) \<rightarrow> (Var a)"
 | s_app: "(App t1 t2) \<rightarrow> (App t1 t2)"