--- a/src/HOL/MicroJava/DFA/Err.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/MicroJava/DFA/Err.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -302,8 +302,8 @@
 done 
 
 text \<open>
-  If @{term "AS = {}"} the thm collapses to
-  @{prop "order r & closed {Err} f & Err +_f Err = Err"}
+  If \<^term>\<open>AS = {}\<close> the thm collapses to
+  \<^prop>\<open>order r & closed {Err} f & Err +_f Err = Err\<close>
   which may not hold 
 \<close>
 lemma err_semilat_UnionI: