diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/UNITY/Union.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -36,7 +36,7 @@
   (*Characterizes safety properties.  Used with specifying Allowed*)
 definition
   safety_prop :: "'a program set => bool"
-  where "safety_prop X \<longleftrightarrow> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
+  where "safety_prop X \<longleftrightarrow> SKIP \<in> X \<and> (\<forall>G. Acts G \<subseteq> UNION X Acts \<longrightarrow> G \<in> X)"
 
 syntax
   "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion>_./ _)" 10)