Manually applied subset_antisym in proof of Compl_fixedpoint, because it is
accidentally applied to predicates as well.

--- a/src/HOL/UNITY/Simple/Reach.thy	Wed May 07 10:59:39 2008 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Wed May 07 10:59:40 2008 +0200
@@ -105,7 +105,8 @@
 
 lemma Compl_fixedpoint: "- fixedpoint = (\<Union>(u,v)\<in>edges. {s. s u & ~ s v})"
 apply (simp add: FP_fixedpoint [symmetric] Rprg_def mk_total_program_def)
-apply (auto simp add: Compl_FP UN_UN_flatten)
+apply (rule subset_antisym)
+apply (auto simp add: Compl_FP UN_UN_flatten del: subset_antisym)
  apply (rule fun_upd_idem, force)
 apply (force intro!: rev_bexI simp add: fun_upd_idem_iff)
 done