diff -r a92d2c915004 -r 66ae73fd66c0 Nominal/NewParser.thy
--- a/Nominal/NewParser.thy	Mon Aug 16 19:57:41 2010 +0800
+++ b/Nominal/NewParser.thy	Tue Aug 17 06:39:27 2010 +0800
@@ -423,9 +423,10 @@
            alpha_intros alpha_induct alpha_cases lthy6
     else raise TEST lthy6
 
-  val alpha_equivp_thms = 
+  val (alpha_equivp_thms, alpha_bn_equivp_thms) = 
     if get_STEPS lthy > 13
-    then raw_prove_equivp alpha_trms alpha_refl_thms alpha_sym_thms alpha_trans_thms lthy6
+    then raw_prove_equivp alpha_trms alpha_bn_trms alpha_refl_thms alpha_sym_thms 
+       alpha_trans_thms lthy6
     else raise TEST lthy6
 
   (* proving alpha implies alpha_bn *)
@@ -450,11 +451,13 @@
 
   val alpha_permute_rsp = map mk_alpha_permute_rsp alpha_eqvt
 
+  val alpha_bn_rsp = raw_alpha_bn_rsp alpha_bn_equivp_thms alpha_bn_imp_thms
+
   (* noting the quot_respects lemmas *)
   val (_, lthy6a) = 
     if get_STEPS lthy > 15
     then Local_Theory.note ((Binding.empty, [rsp_attrib]),
-      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp) lthy6
+      raw_constrs_rsp @ raw_funs_rsp @ raw_size_rsp @ alpha_permute_rsp @ alpha_bn_rsp) lthy6
     else raise TEST lthy6
 
   (* defining the quotient type *)
@@ -534,6 +537,7 @@
      ||>> Local_Theory.note ((@{binding "perm_simps"}, []), raw_perm_simps) 
      ||>> Local_Theory.note ((@{binding "perm_laws"}, []), raw_perm_laws) 
      ||>> Local_Theory.note ((@{binding "alpha_bn_imps"}, []), alpha_bn_imp_thms)
+     ||>> Local_Theory.note ((@{binding "alpha_equivp"}, []), alpha_equivp_thms)
 
   val _ = 
     if get_STEPS lthy > 20