--- a/Nominal/Ex/SingleLet.thy	Sun Aug 29 00:36:47 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 29 01:17:36 2010 +0800
@@ -33,42 +33,16 @@
 thm single_let.fv_bn_eqvt
 thm single_let.size_eqvt
 thm single_let.supports
+thm single_let.fsupp
 
-lemma test:
-  "finite (supp (t::trm)) \<and> finite (supp (a::assg))"
-apply(rule single_let.induct)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-apply(rule supports_finite)
-apply(rule single_let.supports)
-apply(simp only: finite_supp supp_Pair finite_Un, simp)
-done
+
 
 instantiation trm and assg :: fs
 begin
 
 instance
 apply(default)
-apply(simp_all add: test)
+apply(simp_all add: single_let.fsupp)
 done
 
 end