diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/SET_Protocol/Message_SET.thy
--- a/src/HOL/SET_Protocol/Message_SET.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/SET_Protocol/Message_SET.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -21,12 +21,12 @@
 text\<open>Collapses redundant cases in the huge protocol proofs\<close>
 lemmas disj_simps = disj_comms disj_left_absorb disj_assoc 
 
-text\<open>Effective with assumptions like @{term "K \<notin> range pubK"} and 
-   @{term "K \<notin> invKey`range pubK"}\<close>
+text\<open>Effective with assumptions like \<^term>\<open>K \<notin> range pubK\<close> and 
+   \<^term>\<open>K \<notin> invKey`range pubK\<close>\<close>
 lemma notin_image_iff: "(y \<notin> f`I) = (\<forall>i\<in>I. f i \<noteq> y)"
 by blast
 
-text\<open>Effective with the assumption @{term "KK \<subseteq> - (range(invKey o pubK))"}\<close>
+text\<open>Effective with the assumption \<^term>\<open>KK \<subseteq> - (range(invKey o pubK))\<close>\<close>
 lemma disjoint_image_iff: "(A \<subseteq> - (f`I)) = (\<forall>i\<in>I. f i \<notin> A)"
 by blast
 
@@ -263,7 +263,7 @@
 
 
 text\<open>This allows \<open>blast\<close> to simplify occurrences of
-  @{term "parts(G\<union>H)"} in the assumption.\<close>
+  \<^term>\<open>parts(G\<union>H)\<close> in the assumption.\<close>
 declare parts_Un [THEN equalityD1, THEN subsetD, THEN UnE, elim!]