diff -r 0d23a8ae14df -r fbfdc5ac86be src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Sat Sep 10 21:47:55 2011 +0200
+++ b/src/HOL/UNITY/Guar.thy	Sat Sep 10 22:11:55 2011 +0200
@@ -309,8 +309,7 @@
       ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
 apply (unfold guar_def, clarify)
 apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
-apply (auto intro: OK_imp_ok 
-            simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
+apply (auto intro: OK_imp_ok simp add: JN_Join_diff Join_assoc [symmetric])
 done
 
 
@@ -431,9 +430,9 @@
 lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
 apply (unfold ex_prop_def, safe)
  apply (drule_tac x = "G\<squnion>Ga" in spec)
- apply (force simp add: ok_Join_iff1 Join_assoc)
+ apply (force simp add: Join_assoc)
 apply (drule_tac x = "F\<squnion>Ga" in spec)
-apply (simp add: ok_Join_iff1 ok_commute  Join_ac) 
+apply (simp add: ok_commute  Join_ac) 
 done
 
 text{* Equivalence with the other definition of wx *}
@@ -466,7 +465,7 @@
 apply (rule guaranteesI)
 apply (simp add: Join_commute)
 apply (rule stable_Join_Always1)
- apply (simp_all add: invariant_def Join_stable)
+ apply (simp_all add: invariant_def)
 done
 
 lemma constrains_guarantees_leadsTo: