--- a/Nominal/Test.thy	Wed Mar 17 09:25:01 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 09:42:56 2010 +0100
@@ -107,6 +107,7 @@
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
 
+ML {* val _ = cheat_alpha_eqvt := true *}
 ML {* val _ = recursive := true *}
 
 nominal_datatype lam' =
@@ -168,26 +169,11 @@
 apply(simp only: lam'_bp'_perm)
 apply(simp only: permute_ABS)
 apply(simp only: lam'_bp'_inject)
-apply(simp only: eqvts)
 apply(simp only: Abs_eq_iff)
-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(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-apply(simp)
-apply(tactic {* Cong_Tac.cong_tac @{thm cong} 1 *})
-apply(simp)
-apply(rule ext)
-apply(rule sym)
-apply(subgoal_tac "fv_bp' = supp")
-apply(subgoal_tac "fv_lam' = supp")
-apply(simp)
-apply(rule trans)
-apply(rule alpha_abs_Pair[symmetric])
-apply(simp add: alpha_gen supp_Pair)
+apply(simp only: alpha_gen)
+apply(simp only: eqvts split_def fst_conv snd_conv)
+apply(simp only: eqvts[symmetric] supp_Pair)
+apply(simp only: eqvts Pair_eq)
 oops
 
 thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]