diff -r 1ad01f98dc3e -r 67dc9549fa15 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Fri Mar 21 22:54:16 2014 +0100
+++ b/src/HOL/UNITY/Union.thy	Sat Mar 22 08:37:43 2014 +0100
@@ -404,16 +404,16 @@
 by (simp add: stable_def)
 
 lemma safety_prop_Int [simp]:
-     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)"
-by (simp add: safety_prop_def, blast)
+  "safety_prop X \<Longrightarrow> safety_prop Y \<Longrightarrow> safety_prop (X \<inter> Y)"
+  by (simp add: safety_prop_def) blast
+
+lemma safety_prop_INTER [simp]:
+  "(\<And>i. i \<in> I \<Longrightarrow> safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i\<in>I. X i)"
+  by (simp add: safety_prop_def) blast
 
 lemma safety_prop_INTER1 [simp]:
-     "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
-by (auto simp add: safety_prop_def, blast)
-
-lemma safety_prop_INTER [simp]:
-     "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
-by (auto simp add: safety_prop_def, blast)
+  "(\<And>i. safety_prop (X i)) \<Longrightarrow> safety_prop (\<Inter>i. X i)"
+  by (rule safety_prop_INTER) simp
 
 lemma def_prg_Allowed:
      "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |]