--- 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