--- a/Nominal/NewParser.thy	Thu Aug 12 21:29:35 2010 +0800
+++ b/Nominal/NewParser.thy	Sat Aug 14 16:54:41 2010 +0800
@@ -438,15 +438,19 @@
     then raw_prove_bn_imp alpha_trms alpha_bn_trms alpha_intros alpha_induct lthy6 
     else raise TEST lthy6
   
-  (* auxiliary lemmas for respectfulness proofs *)
-  val raw_funs_rsp = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
+  (* respectfulness proofs *)
+  val raw_funs_rsp_aux = raw_fv_bn_rsp_aux alpha_trms alpha_bn_trms raw_fvs 
     raw_bns raw_fv_bns alpha_induct (raw_bn_eqs @ raw_fv_defs) lthy6
+  val raw_funs_rsp = map mk_funs_rsp raw_funs_rsp_aux
 
   val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
     (raw_size_thms @ raw_size_eqvt) lthy6
+    |> map mk_funs_rsp
 
   val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros
-    (alpha_bn_imp_thms @ raw_funs_rsp) lthy6 
+    (alpha_bn_imp_thms @ raw_funs_rsp_aux) lthy6 
+
+  val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -508,13 +512,10 @@
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
      ||>> Local_Theory.note ((@{binding "funs_rsp"}, []), raw_funs_rsp)
-     ||>> Local_Theory.note ((@{binding "size_eqvt"}, []), raw_size_eqvt)
-     ||>> Local_Theory.note ((@{binding "size_simps"}, []), raw_size_thms)
      ||>> Local_Theory.note ((@{binding "size_rsp"}, []), raw_size_rsp)
      ||>> Local_Theory.note ((@{binding "constrs_rsp"}, []), raw_constrs_rsp)
-     ||>> Local_Theory.note ((@{binding "alpha_sym_thms"}, []), alpha_sym_thms)
-     ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms)
-  
+     ||>> Local_Theory.note ((@{binding "permute_rsp"}, []), alpha_permute_rsp)
+
   val _ = 
     if get_STEPS lthy > 17
     then true else raise TEST lthy8'