--- a/Nominal/Test.thy	Thu Mar 18 11:37:10 2010 +0100
+++ b/Nominal/Test.thy	Thu Mar 18 12:09:59 2010 +0100
@@ -23,13 +23,13 @@
 lemma finite_fv:
   shows "finite (fv_lm t)"
 apply(induct t rule: lm_induct)
-apply(simp_all add: lm_fv)
+apply(simp_all)
 done
 
 lemma supp_fn:
   shows "supp t = fv_lm t"
 apply(induct t rule: lm_induct)
-apply(simp_all add: lm_fv)
+apply(simp_all)
 apply(simp only: supp_def)
 apply(simp only: lm_perm)
 apply(simp only: lm_eq_iff)
@@ -77,7 +77,7 @@
     apply(erule exE)
     apply(rule_tac t="p \<bullet> Lm name lm" and 
                    s="(((p \<bullet> name) \<leftrightarrow> new) + p) \<bullet> Lm name lm" in subst)
-    apply(simp)
+    apply(simp del: lm_perm)
     apply(subst lm_perm)
     apply(subst (2) lm_perm)
     apply(rule flip_fresh_fresh)
@@ -85,7 +85,7 @@
     apply(simp only: supp_fn')
     apply(simp)
     apply(simp add: fresh_Pair)
-    apply(simp add: lm_perm)
+    apply(simp)
     apply(rule a3)
     apply(drule_tac x="((p \<bullet> name) \<leftrightarrow> new) + p" in meta_spec)
     apply(simp)
@@ -130,7 +130,7 @@
   shows "supp t = fv_lam t" 
   and "supp bp = fv_bp bp \<and> fv_bi bp = {a. infinite {b. \<not>alpha_bi ((a \<rightleftharpoons> b) \<bullet> bp) bp}}"
 apply(induct t and bp rule: lam_bp_inducts)
-apply(simp_all add: lam_bp_fv)
+apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: lam_bp_perm)
@@ -218,7 +218,7 @@
   shows "supp t = fv_lam' t" 
   and "supp bp = fv_bp' bp"
 apply(induct t and bp rule: lam'_bp'_inducts)
-apply(simp_all add: lam'_bp'_fv)
+apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: lam'_bp'_perm)
@@ -304,7 +304,7 @@
   shows "supp t = fv_trm' t" 
   and "supp bp = fv_pat' bp \<and> {a. infinite {b. \<not>alpha_f ((a \<rightleftharpoons> b) \<bullet> bp) bp}} = fv_f bp"
 apply(induct t and bp rule: trm'_pat'_inducts)
-apply(simp_all add: trm'_pat'_fv)
+apply(simp_all)
 (* VAR case *)
 apply(simp only: supp_def)
 apply(simp only: trm'_pat'_perm)
@@ -439,7 +439,7 @@
   shows "supp T = fv_t T" 
   and   "supp S = fv_tyS S"
 apply(induct T and S rule: t_tyS_inducts)
-apply(simp_all add: t_tyS_fv)
+apply(simp_all)
 (* VarTS case *)
 apply(simp only: supp_def)
 apply(simp only: t_tyS_perm)
@@ -519,11 +519,6 @@
 thm trm3_rassigns3_induct
 thm trm3_rassigns3_distinct
 
-(* compat should be
-compat (ANil) pi (PNil) \<equiv> TRue
-compat (ACons x t ts) pi (ACons x' t' ts') \<equiv> pi o x = x' \<and> alpha t t' \<and> compat ts pi ts'
-*)
-
 (* example 5 from Terms.thy *)
 
 nominal_datatype trm5 =