--- a/Nominal/Ex/SingleLet.thy	Sat Jul 31 02:10:42 2010 +0100
+++ b/Nominal/Ex/SingleLet.thy	Sun Aug 08 10:12:38 2010 +0800
@@ -24,6 +24,8 @@
 thm alpha_sym_thms
 thm alpha_trans_thms
 thm size_eqvt
+thm size_simps
+thm size_rsp
 thm alpha_bn_imps
 thm distinct
 thm eq_iff
@@ -43,7 +45,6 @@
 term fv_trm
 term alpha_bn
 
-
 lemma exi_zero: "P 0 \<Longrightarrow> \<exists>(x::perm). P x" by auto
 
 ML {* 
@@ -77,7 +78,8 @@
   "(alpha_assg_raw ===> op =) bn_raw bn_raw"
   "(alpha_assg_raw ===> op =) fv_assg_raw fv_assg_raw"
   "(op = ===> alpha_trm_raw ===> alpha_trm_raw) permute permute"
-apply(simp_all add: alpha_bn_imps funs_rsp)
+  "(alpha_trm_raw ===> op =) size size"
+apply(simp_all add: alpha_bn_imps funs_rsp size_rsp)
 sorry
 
 ML {*