--- a/src/HOL/MicroJava/BV/Correct.thy	Fri Sep 20 19:07:10 2024 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Fri Sep 20 19:51:08 2024 +0200
@@ -42,7 +42,7 @@
      correct_frames G hp phi rT sig frs))))"
 
 definition correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
-                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50) where
+                  (\<open>_,_ \<turnstile>JVM _ \<surd>\<close>  [51,51] 50) where
 "correct_state G phi == \<lambda>(xp,hp,frs).
    case xp of
      None \<Rightarrow> (case frs of