src/HOL/MicroJava/BV/BVSpec.thy

--- a/src/HOL/MicroJava/BV/BVSpec.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/MicroJava/BV/BVSpec.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -97,8 +97,8 @@
       simp, simp, simp add: wf_mdecl_def wt_method_def)
 
 text \<open>
-  We could leave out the check @{term "pc' < max_pc"} in the 
-  definition of @{term wt_instr} in the context of @{term wt_method}.
+  We could leave out the check \<^term>\<open>pc' < max_pc\<close> in the 
+  definition of \<^term>\<open>wt_instr\<close> in the context of \<^term>\<open>wt_method\<close>.
 \<close>
 lemma wt_instr_def2:
   "\<lbrakk> wt_jvm_prog G Phi; is_class G C;