src/HOL/UNITY/Transformers.thy

--- a/src/HOL/UNITY/Transformers.thy	Tue Aug 09 18:52:18 2011 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Tue Aug 09 20:24:48 2011 +0200
@@ -467,7 +467,7 @@
       "single_valued act
        ==> insert (wens_single act B) (range (wens_single_finite act B)) \<subseteq> 
            wens_set (mk_program (init, {act}, allowed)) B"
-apply (simp add: wens_single_eq_Union UN_eq) 
+apply (simp add: SUP_def image_def wens_single_eq_Union) 
 apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
 done