diff -r bccda961a612 -r 1a6593bc494d Nominal/Nominal2.thy
--- a/Nominal/Nominal2.thy	Tue May 24 19:39:38 2011 +0200
+++ b/Nominal/Nominal2.thy	Wed May 25 21:38:50 2011 +0200
@@ -43,6 +43,7 @@
 val eqvt_attr = Attrib.internal (K Nominal_ThmDecls.eqvt_add)
 val rsp_attr = Attrib.internal (K Quotient_Info.rsp_rules_add)
 val simp_attr = Attrib.internal (K Simplifier.simp_add)
+val induct_attr = Attrib.internal (K Induct.induct_simp_add)
 *}
 
 section{* Interface for nominal_datatype *}
@@ -455,8 +456,8 @@
   val case_names_attr = Attrib.internal (K (Rule_Cases.case_names cnstr_names))
 
   val (_, lthy9') = lthyC
-     |> Local_Theory.note ((thms_suffix "distinct", []), qdistincts) 
-     ||>> Local_Theory.note ((thms_suffix "eq_iff", []), qeq_iffs')
+     |> Local_Theory.note ((thms_suffix "distinct", [induct_attr, simp_attr]), qdistincts) 
+     ||>> Local_Theory.note ((thms_suffix "eq_iff", [induct_attr, simp_attr]), qeq_iffs')
      ||>> Local_Theory.note ((thms_suffix "fv_defs", []), qfv_defs) 
      ||>> Local_Theory.note ((thms_suffix "bn_defs", []), qbn_defs) 
      ||>> Local_Theory.note ((thms_suffix "perm_simps", [eqvt_attr, simp_attr]), qperm_simps)