--- a/Nominal/Term1.thy	Fri Mar 12 17:42:31 2010 +0100
+++ b/Nominal/Term1.thy	Sat Mar 13 13:49:15 2010 +0100
@@ -262,6 +262,8 @@
 apply (simp add: atom_eqvt[symmetric])
 sorry
 
+thm trm1_bp_inducts
+
 lemma supp_fv:
   "supp t = fv_trm1 t"
   "supp b = fv_bp b"
@@ -280,9 +282,7 @@
 apply(simp add: supp_eqvt[symmetric] fv_trm1_eqvt[symmetric])
 defer
 apply(simp (no_asm) add: supp_def permute_set_eq atom_eqvt)
-apply(simp (no_asm) add: supp_def eqvts)
-apply(fold supp_def)
-apply(simp add: supp_at_base)
+apply(simp only: supp_at_base[simplified supp_def])
 apply(simp (no_asm) add: supp_def Collect_imp_eq Collect_neg_eq)
 apply(simp add: Collect_imp_eq[symmetric] Collect_neg_eq[symmetric] supp_def[symmetric])
 (*apply(rule supp_fv_let) apply(simp_all)*)
@@ -300,8 +300,6 @@
 apply(simp only: ex_out)
 apply(simp only: Collect_neg_conj finite_Un Diff_cancel)
 apply(simp)
-apply(simp add: Collect_imp_eq)
-apply(simp add: Collect_neg_eq[symmetric] fresh_star_def)
 apply(fold supp_def)
 sorry