diff -r 46f59511b7bb -r d97fdabd9e2b src/HOL/MicroJava/BV/BVExample.thy
--- a/src/HOL/MicroJava/BV/BVExample.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/MicroJava/BV/BVExample.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -163,7 +163,7 @@
 
   @{prop [display] "P n"} 
 \<close>
-definition intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')") where
+definition intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" (\<open>_ \<in> [_, _')\<close>) where
   "x \<in> [a, b) \<equiv> a \<le> x \<and> x < b"
 
 lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x"
@@ -233,7 +233,7 @@
 lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def
 declare appInvoke [simp del]
 
-definition phi_append :: method_type ("\<phi>\<^sub>a") where
+definition phi_append :: method_type (\<open>\<phi>\<^sub>a\<close>) where
   "\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ 
    (                                    [], [Class list_name, Class list_name]),
    (                     [Class list_name], [Class list_name, Class list_name]),
@@ -295,7 +295,7 @@
 abbreviation Ctest :: ty
   where "Ctest == Class test_name"
 
-definition phi_makelist :: method_type ("\<phi>\<^sub>m") where
+definition phi_makelist :: method_type (\<open>\<phi>\<^sub>m\<close>) where
   "\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ 
     (                                   [], [OK Ctest, Err     , Err     ]),
     (                              [Clist], [OK Ctest, Err     , Err     ]),
@@ -369,7 +369,7 @@
   done
 
 text \<open>The whole program is welltyped:\<close>
-definition Phi :: prog_type ("\<Phi>") where
+definition Phi :: prog_type (\<open>\<Phi>\<close>) where
   "\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else          
              if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []"