--- 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))"