diff -r b4ea19604b0b -r fbdaaa20396b Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sat Sep 25 08:28:45 2010 -0400
+++ b/Nominal/Nominal2.thy	Sat Sep 25 08:38:04 2010 -0400
@@ -529,13 +529,14 @@
       ||>> lift_thms qtys [] (raw_fv_eqvt @ raw_bn_eqvt)
     else raise TEST lthy9a
 
-  val (((qsize_eqvt, [qinduct]), qexhausts), lthyB) = 
+  val ((((qsize_eqvt, [qinduct]), qexhausts), qsize_simps), lthyB) = 
     if get_STEPS lthy > 27
     then
       lthyA 
       |> lift_thms qtys [] raw_size_eqvt
       ||>> lift_thms qtys [] [raw_induct_thm]
       ||>> lift_thms qtys [] raw_exhaust_thms
+      ||>> lift_thms qtys [] raw_size_thms
     else raise TEST lthyA
 
   val qinducts = Project_Rule.projections lthyA qinduct
@@ -582,6 +583,7 @@
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps) 
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
+     ||>> Local_Theory.note ((thms_suffix "size", []), qsize_simps)
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
      ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)