diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Metis_Examples/Message.thy
--- a/src/HOL/Metis_Examples/Message.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Metis_Examples/Message.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -217,7 +217,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>
 lemmas in_parts_UnE = parts_Un [THEN equalityD1, THEN subsetD, THEN UnE]
 declare in_parts_UnE [elim!]
 
@@ -461,8 +461,8 @@
 
 text\<open>Case analysis: either the message is secure, or it is not! Effective,
 but can cause subgoals to blow up! Use with \<open>if_split\<close>; apparently
-\<open>split_tac\<close> does not cope with patterns such as @{term"analz (insert
-(Crypt K X) H)"}\<close>
+\<open>split_tac\<close> does not cope with patterns such as \<^term>\<open>analz (insert
+(Crypt K X) H)\<close>\<close>
 lemma analz_Crypt_if [simp]:
      "analz (insert (Crypt K X) H) =
           (if (Key (invKey K) \<in> analz H)
@@ -576,7 +576,7 @@
   by (auto, erule synth.induct, auto)
 
 text\<open>NO \<open>Agent_synth\<close>, as any Agent name can be synthesized.
-  The same holds for @{term Number}\<close>
+  The same holds for \<^term>\<open>Number\<close>\<close>
 inductive_cases Nonce_synth [elim!]: "Nonce n \<in> synth H"
 inductive_cases Key_synth   [elim!]: "Key K \<in> synth H"
 inductive_cases Hash_synth  [elim!]: "Hash X \<in> synth H"