--- a/Nominal/Test.thy	Wed Mar 17 09:42:56 2010 +0100
+++ b/Nominal/Test.thy	Wed Mar 17 09:57:54 2010 +0100
@@ -131,7 +131,7 @@
 thm lam'_bp'_distinct
 ML {* Sign.of_sort @{theory} (@{typ lam'}, @{sort fs}) *}
 
-lemma supp_fv:
+lemma supp_fv':
   shows "supp t = fv_lam' t" 
   and "supp bp = fv_bp' bp"
 apply(induct t and bp rule: lam'_bp'_inducts)
@@ -174,9 +174,21 @@
 apply(simp only: eqvts split_def fst_conv snd_conv)
 apply(simp only: eqvts[symmetric] supp_Pair)
 apply(simp only: eqvts Pair_eq)
-oops
+apply(simp add: supp_Abs supp_Pair)
+apply blast
+apply(simp only: supp_def)
+apply(simp only: lam'_bp'_perm)
+apply(simp only: lam'_bp'_inject)
+apply(simp only: de_Morgan_conj)
+apply(simp only: Collect_disj_eq)
+apply(simp only: infinite_Un)
+apply(simp only: Collect_disj_eq)
+apply(simp only: supp_def[symmetric])
+apply(simp only: supp_at_base supp_atom)
+apply simp
+done
 
-thm lam_bp_fv[simplified supp_fv(1)[symmetric] supp_fv(2)[THEN conjunct1, symmetric]]
+thm lam'_bp'_fv[simplified supp_fv'[symmetric]]
 
 
 text {* example 2 *}