--- a/Nominal/Term1.thy	Thu Mar 11 17:47:29 2010 +0100
+++ b/Nominal/Term1.thy	Thu Mar 11 17:49:07 2010 +0100
@@ -140,13 +140,9 @@
 apply(tactic {* ALLGOALS (supports_tac @{thms permute_trm1}) *})
 done
 
-lemma rtrm1_bp_fs:
-  "finite (supp (x :: trm1))"
-  "finite (supp (b :: bp))"
-  apply (induct x and b rule: trm1_bp_inducts)
-  apply(tactic {* ALLGOALS (rtac @{thm supports_finite} THEN' resolve_tac @{thms supports}) *})
-  apply(simp_all add: supp_atom)
-  done
+prove rtrm1_bp_fs: {* snd (mk_fs [@{typ trm1}, @{typ bp}]) *}
+apply (tactic {* fs_tac @{thm trm1_bp_induct} @{thms supports} 1 *})
+done
 
 instance trm1 and bp :: fs
 apply default