diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/MicroJava/JVM/JVMExceptions.thy
--- a/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/MicroJava/JVM/JVMExceptions.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -48,7 +48,7 @@
 
 text \<open>
   Only program counters that are mentioned in the exception table
-  can be returned by @{term match_exception_table}:
+  can be returned by \<^term>\<open>match_exception_table\<close>:
 \<close>
 lemma match_exception_table_in_et:
   "match_exception_table G C pc et = Some pc' \<Longrightarrow> \<exists>e \<in> set et. pc' = fst (snd (snd e))"