--- a/Nominal/NewParser.thy	Wed Aug 11 16:23:50 2010 +0800
+++ b/Nominal/NewParser.thy	Wed Aug 11 19:53:57 2010 +0800
@@ -445,6 +445,8 @@
   val raw_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
     (raw_size_thms @ raw_size_eqvt) lthy6
 
+  val raw_constrs_rsp = raw_constrs_rsp all_raw_constrs alpha_trms alpha_intros
+    (alpha_bn_imp_thms @ raw_funs_rsp) lthy6 
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -509,6 +511,7 @@
      ||>> 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)