--- a/Nominal/Nominal2.thy	Tue Dec 28 00:20:50 2010 +0000
+++ b/Nominal/Nominal2.thy	Tue Dec 28 19:51:25 2010 +0000
@@ -535,7 +535,7 @@
   val qstrong_exhaust_thms = prove_strong_exhausts lthyC qexhausts bclauses qbn_finite_thms qeq_iffs'
     qfv_qbn_eqvts qpermute_bn_thms qperm_bn_alpha_thms
 
-  val qstrong_induct_thm = prove_strong_induct lthyC qinduct qstrong_exhaust_thms bclauses
+  val qstrong_induct_thms = prove_strong_induct lthyC qinduct qstrong_exhaust_thms qsize_simps bclauses
 
 
   (* noting the theorems *)  
@@ -558,6 +558,7 @@
      ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts)
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "strong_exhaust", []), qstrong_exhaust_thms)
+     ||>> Local_Theory.note ((thms_suffix "strong_induct", []), qstrong_induct_thms)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)
      ||>> Local_Theory.note ((thms_suffix "supp", []), qsupp_constrs)