--- a/Nominal/Test.thy	Mon Mar 15 08:39:23 2010 +0100
+++ b/Nominal/Test.thy	Mon Mar 15 09:27:25 2010 +0100
@@ -35,13 +35,7 @@
 
 lemma bi_eqvt:
   shows "(p \<bullet> (bi b)) = bi (p \<bullet> b)"
-apply(induct b rule: lam_bp_inducts(2))
-apply(simp)
-apply(simp)
-apply(simp)
-apply(simp add: lam_bp_bn lam_bp_perm)
-apply(simp add: eqvts)
-done
+  by (rule eqvts)
 
 lemma supp_fv:
   "supp t = fv_lam t" and