src/HOL/UNITY/ProgressSets.thy

--- a/src/HOL/UNITY/ProgressSets.thy	Sat Mar 15 16:54:32 2014 +0100
+++ b/src/HOL/UNITY/ProgressSets.thy	Sun Mar 16 18:09:04 2014 +0100
@@ -257,7 +257,7 @@
  apply (simp add: progress_induction_step) 
 txt{*Disjunctive case*}
 apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
- apply (simp add: Int_Union) 
+ apply simp 
 apply (blast intro: UN_in_lattice) 
 done