--- a/Nominal/Term1.thy	Sun Mar 07 21:30:57 2010 +0100
+++ b/Nominal/Term1.thy	Mon Mar 08 02:40:16 2010 +0100
@@ -232,6 +232,7 @@
 apply(simp only: Un_commute)
 apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *}) apply(rule refl)
 apply(simp only: Collect_disj_eq[symmetric] inf_or)
+apply(simp only: HOL.imp_disj2[symmetric] HOL.not_ex[symmetric] HOL.disj_not1[symmetric] HOL.de_Morgan_conj[symmetric])
 sorry
 
 lemma supp_fv: