--- a/Nominal/Ex/Foo2.thy	Fri Dec 03 13:51:07 2010 +0000
+++ b/Nominal/Ex/Foo2.thy	Mon Dec 06 14:24:17 2010 +0000
@@ -24,7 +24,9 @@
  "bn (As x y t a) = [atom x] @ bn a"
 | "bn (As_Nil) = []"
 
+thm foo.perm_bn_alpha
 thm foo.perm_bn_simps
+thm foo.bn_finite
 
 thm foo.distinct
 thm foo.induct
@@ -45,19 +47,23 @@
   shows "alpha_bn as (permute_bn p as)"
 apply(induct as rule: foo.inducts(2))
 apply(auto)[5]
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
-apply(simp add: foo.perm_bn_simps)
-apply(simp add: foo.eq_iff)
+apply(simp only: foo.perm_bn_simps)
+apply(simp only: foo.eq_iff)
+apply(simp only: foo.perm_bn_simps)
+apply(simp only: foo.eq_iff refl)
+apply(simp)
 done
 
 lemma tt1:
   shows "(p \<bullet> bn as) = bn (permute_bn p as)"
 apply(induct as rule: foo.inducts(2))
 apply(auto)[5]
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: foo.perm_bn_simps foo.bn_defs)
-apply(simp add: atom_eqvt)
+apply(simp only: foo.perm_bn_simps foo.bn_defs)
+apply(perm_simp)
+apply(simp only:)
+apply(simp only: foo.perm_bn_simps foo.bn_defs)
+apply(perm_simp add: foo.fv_bn_eqvt)
+apply(simp only:)
 done
 
 text {*