--- a/Nominal/Ex/SingleLet.thy	Sun Aug 08 10:12:38 2010 +0800
+++ b/Nominal/Ex/SingleLet.thy	Wed Aug 11 16:21:24 2010 +0800
@@ -35,6 +35,8 @@
 thm perm_laws
 thm funs_rsp
 
+declare size_rsp[quot_respect]
+declare funs_rsp[quot_respect]
 
 typ trm
 typ assg
@@ -70,16 +72,11 @@
   "(op= ===> alpha_trm_raw ===> alpha_trm_raw ===> alpha_trm_raw) Baz_raw Baz_raw"
   "(op = ===> op = ===> alpha_trm_raw ===> alpha_assg_raw) As_raw As_raw"
 apply(tactic {* ALLGOALS tac *})
-done
+sorry
 
 lemma [quot_respect]:
-  "(alpha_trm_raw ===> op =) fv_trm_raw fv_trm_raw"
-  "(alpha_assg_raw ===> op =) fv_bn_raw fv_bn_raw"
-  "(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"
-  "(alpha_trm_raw ===> op =) size size"
-apply(simp_all add: alpha_bn_imps funs_rsp size_rsp)
+apply(simp)
 sorry
 
 ML {*