diff -r a80d8ec6c998 -r 3dda49e08b9d src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Fri Jan 04 21:49:06 2019 +0100
+++ b/src/HOL/Transitive_Closure.thy	Fri Jan 04 23:22:53 2019 +0100
@@ -173,7 +173,7 @@
 
 lemmas converse_rtrancl_into_rtrancl = converse_rtranclp_into_rtranclp [to_set]
 
-text \<open>\<^medskip> More @{term "r\<^sup>*"} equations and inclusions.\<close>
+text \<open>\<^medskip> More \<^term>\<open>r\<^sup>*\<close> equations and inclusions.\<close>
 
 lemma rtranclp_idemp [simp]: "(r\<^sup>*\<^sup>*)\<^sup>*\<^sup>* = r\<^sup>*\<^sup>*"
   apply (auto intro!: order_antisym)
@@ -391,7 +391,7 @@
 lemma trancl_unfold: "r\<^sup>+ = r \<union> r\<^sup>+ O r"
   by (auto intro: trancl_into_trancl elim: tranclE)
 
-text \<open>Transitivity of @{term "r\<^sup>+"}\<close>
+text \<open>Transitivity of \<^term>\<open>r\<^sup>+\<close>\<close>
 lemma trans_trancl [simp]: "trans (r\<^sup>+)"
 proof (rule transI)
   fix x y z
@@ -1226,10 +1226,10 @@
 
   fun decomp (@{const Trueprop} $ t) =
         let
-          fun dec (Const (@{const_name Set.member}, _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel) =
+          fun dec (Const (\<^const_name>\<open>Set.member\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ a $ b) $ rel) =
               let
-                fun decr (Const (@{const_name rtrancl}, _ ) $ r) = (r,"r*")
-                  | decr (Const (@{const_name trancl}, _ ) $ r)  = (r,"r+")
+                fun decr (Const (\<^const_name>\<open>rtrancl\<close>, _ ) $ r) = (r,"r*")
+                  | decr (Const (\<^const_name>\<open>trancl\<close>, _ ) $ r)  = (r,"r+")
                   | decr r = (r,"r");
                 val (rel,r) = decr (Envir.beta_eta_contract rel);
               in SOME (a,b,rel,r) end
@@ -1253,8 +1253,8 @@
         let
           fun dec (rel $ a $ b) =
             let
-              fun decr (Const (@{const_name rtranclp}, _ ) $ r) = (r,"r*")
-                | decr (Const (@{const_name tranclp}, _ ) $ r)  = (r,"r+")
+              fun decr (Const (\<^const_name>\<open>rtranclp\<close>, _ ) $ r) = (r,"r*")
+                | decr (Const (\<^const_name>\<open>tranclp\<close>, _ ) $ r)  = (r,"r+")
                 | decr r = (r,"r");
               val (rel,r) = decr rel;
             in SOME (a, b, rel, r) end