diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/MicroJava/DFA/Typing_Framework_err.thy
--- a/src/HOL/MicroJava/DFA/Typing_Framework_err.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/MicroJava/DFA/Typing_Framework_err.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -161,8 +161,8 @@
 text \<open>
   There used to be a condition here that each instruction must have a
   successor. This is not needed any more, because the definition of
-  @{term error} trivially ensures that there is a successor for
-  the critical case where @{term app} does not hold. 
+  \<^term>\<open>error\<close> trivially ensures that there is a successor for
+  the critical case where \<^term>\<open>app\<close> does not hold. 
 \<close>
 lemma wt_err_imp_wt_app_eff:
   assumes wt: "wt_err_step r (err_step (size ts) app step) ts"