--- a/Nominal/NewParser.thy	Sat Jul 31 02:10:42 2010 +0100
+++ b/Nominal/NewParser.thy	Sun Aug 08 10:12:38 2010 +0800
@@ -322,7 +322,7 @@
   val raw_size_trms = map (fn ty => Const (@{const_name size}, ty --> @{typ nat})) all_raw_tys
   val raw_size_thms = Size.size_thms (ProofContext.theory_of lthy0) (hd raw_dt_names)
     |> `(fn thms => (length thms) div 2)
-    |> (uncurry drop)
+    |> uncurry drop
   
 
   (* definitions of raw permutations *)
@@ -442,6 +442,9 @@
   val raw_funs_rsp = 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_size_rsp = raw_size_rsp_aux (alpha_trms @ alpha_bn_trms) alpha_induct 
+    (raw_size_thms @ raw_size_eqvt) lthy6
+
 
   (* defining the quotient type *)
   val _ = warning "Declaring the quotient types"
@@ -504,6 +507,8 @@
      ||>> 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 "alpha_sym_thms"}, []), alpha_sym_thms)
      ||>> Local_Theory.note ((@{binding "alpha_trans_thms"}, []), alpha_trans_thms)