--- a/Nominal/Test.thy	Tue Mar 16 12:06:22 2010 +0100
+++ b/Nominal/Test.thy	Tue Mar 16 12:08:37 2010 +0100
@@ -129,16 +129,9 @@
 apply(simp only: alpha_tst) 
 apply(simp only: supp_eqvt[symmetric])
 apply(simp only: eqvts)
-defer (* hacking *)
+apply simp
 apply(simp add: supp_Abs_tst)
 apply(simp add: fv_bi)
-apply(rule Collect_cong)
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-apply(simp)
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-apply(simp)
-apply(rule Collect_cong)
-apply(blast)
 done
 
 text {* example 2 *}