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