diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Transitive_Closure.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -1224,7 +1224,7 @@
   val trancl_rtrancl_trancl = @{thm trancl_rtrancl_trancl};
   val rtrancl_trans = @{thm rtrancl_trans};
 
-  fun decomp (@{const Trueprop} $ t) =
+  fun decomp (\<^const>\<open>Trueprop\<close> $ t) =
         let
           fun dec (Const (\<^const_name>\<open>Set.member\<close>, _) $ (Const (\<^const_name>\<open>Pair\<close>, _) $ a $ b) $ rel) =
               let
@@ -1249,7 +1249,7 @@
   val trancl_rtrancl_trancl = @{thm tranclp_rtranclp_tranclp};
   val rtrancl_trans = @{thm rtranclp_trans};
 
-  fun decomp (@{const Trueprop} $ t) =
+  fun decomp (\<^const>\<open>Trueprop\<close> $ t) =
         let
           fun dec (rel $ a $ b) =
             let