--- a/Nominal/Nominal2.thy	Tue Jul 12 03:12:32 2011 +0900
+++ b/Nominal/Nominal2.thy	Wed Jul 13 09:47:58 2011 +0100
@@ -328,7 +328,7 @@
   val alpha_bn_rsp = 
     raw_alpha_bn_rsp alpha_result alpha_bn_equivp_thms alpha_bn_imp_thms
 
-  val raw_perm_bn_rsp =raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
+  val raw_perm_bn_rsp = raw_perm_bn_rsp lthy5 alpha_result raw_perm_bns raw_perm_bn_simps
 
   (* noting the quot_respects lemmas *)
   val (_, lthy6) = 
@@ -408,7 +408,7 @@
 
   val ([ qdistincts, qeq_iffs, qfv_defs, qbn_defs, qperm_simps, qfv_qbn_eqvts, 
          qbn_inducts, qsize_eqvt, [qinduct], qexhausts, qsize_simps, qperm_bn_simps, 
-         qalpha_refl_thms ], lthyB) = 
+         qalpha_refl_thms, qalpha_sym_thms, qalpha_trans_thms ], lthyB) = 
     lthy9a    
     |>>> lift_thms qtys [] alpha_distincts  
     ||>>> lift_thms qtys eq_iff_simps alpha_eq_iff       
@@ -423,6 +423,8 @@
     ||>>> lift_thms qtys [] raw_size_thms
     ||>>> lift_thms qtys [] raw_perm_bn_simps
     ||>>> lift_thms qtys [] alpha_refl_thms
+    ||>>> lift_thms qtys [] alpha_sym_thms
+    ||>>> lift_thms qtys [] alpha_trans_thms
 
   val qinducts = Project_Rule.projections lthyB qinduct
 
@@ -512,6 +514,10 @@
      ||>> Local_Theory.note ((thms_suffix "bn_finite", []), qbn_finite_thms)
      ||>> Local_Theory.note ((thms_suffix "perm_bn_alpha", []), qperm_bn_alpha_thms)
      ||>> Local_Theory.note ((thms_suffix "permute_bn", []), qpermute_bn_thms)
+     ||>> Local_Theory.note ((thms_suffix "alpha_refl", []), qalpha_refl_thms)
+     ||>> Local_Theory.note ((thms_suffix "alpha_sym", []), qalpha_sym_thms)
+     ||>> Local_Theory.note ((thms_suffix "alpha_trans", []), qalpha_trans_thms)
+     
 in
   lthy9'
 end