diff -r a3711f07449b -r 6e37bfb62474 Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Sun Sep 05 06:42:53 2010 +0800
+++ b/Nominal/Nominal2.thy	Sun Sep 05 07:00:19 2010 +0800
@@ -539,6 +539,8 @@
       ||>> lift_thms qtys [] raw_exhaust_thms
     else raise TEST lthyA
 
+  val qinducts = Project_Rule.projections lthyA qinduct
+
   (* supports lemmas *) 
   val qsupports_thms =
     if get_STEPS lthy > 28
@@ -573,6 +575,7 @@
      ||>> Local_Theory.note ((thms_suffix "fv_bn_eqvt", []), qfv_qbn_eqvts) 
      ||>> Local_Theory.note ((thms_suffix "size_eqvt", []), qsize_eqvt)
      ||>> Local_Theory.note ((thms_suffix "induct", []), [qinduct]) 
+     ||>> Local_Theory.note ((thms_suffix "inducts", []), qinducts) 
      ||>> Local_Theory.note ((thms_suffix "exhaust", []), qexhausts)
      ||>> Local_Theory.note ((thms_suffix "supports", []), qsupports_thms)
      ||>> Local_Theory.note ((thms_suffix "fsupp", []), qfsupp_thms)