diff -r 666774b0d1b0 -r c6d81ddebb0e src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Fri Jul 01 14:14:40 2005 +0200
+++ b/src/HOL/UNITY/Guar.thy	Fri Jul 01 14:16:32 2005 +0200
@@ -431,7 +431,7 @@
 by (unfold wx_def, auto)
 
 lemma wx_ex_prop: "ex_prop (wx X)"
-apply (simp add: wx_def ex_prop_equiv, safe, blast)
+apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast)
 apply force 
 done