src/HOL/TLA/TLA.thy

--- a/src/HOL/TLA/TLA.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/TLA/TLA.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -116,7 +116,7 @@
 
 fun temp_use ctxt th =
   case Thm.concl_of th of
-    Const _ $ (Const (@{const_name Intensional.Valid}, _) $ _) =>
+    Const _ $ (Const (\<^const_name>\<open>Intensional.Valid\<close>, _) $ _) =>
             ((flatten (temp_unlift ctxt th)) handle THM _ => th)
   | _ => th;