src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Orderings.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -512,7 +512,7 @@
 fun struct_tac ((s, ops), thms) ctxt facts =
   let
     val [eq, le, less] = ops;
-    fun decomp thy (@{const Trueprop} $ t) =
+    fun decomp thy (\<^const>\<open>Trueprop\<close> $ t) =
           let
             fun excluded t =
               (* exclude numeric types: linear arithmetic subsumes transitivity *)