--- a/Nominal/Term1.thy	Thu Mar 11 16:50:44 2010 +0100
+++ b/Nominal/Term1.thy	Thu Mar 11 17:47:29 2010 +0100
@@ -137,11 +137,7 @@
   "{} supports BUnit"
   "(supp (atom x)) supports (BVr x)"
   "(supp a \<union> supp b) supports (BPr a b)"
-apply(simp_all add: supports_def fresh_def[symmetric] swap_fresh_fresh permute_trm1)
-apply(rule_tac [!] allI)+
-apply(rule_tac [!] impI)
-apply(tactic {* ALLGOALS (REPEAT o etac conjE) *})
-apply(simp_all add: fresh_atom)
+apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *})
 done
 
 lemma rtrm1_bp_fs: