src/ZF/Tools/datatype_package.ML

  in
   (*Updating theory components: simprules and datatype info*)
   (thy1 |> Theory.add_path big_rec_base_name
         |> PureThy.add_thmss [(("simps", simps), 
 			       [Simplifier.simp_add_global])]
-        |> PureThy.add_thmss [(("intrs", intrs), 
+        |> PureThy.add_thmss [(("", intrs),   
+                                (*not "intrs" to avoid the warning that they
+				  are already stored by the inductive package*)
 			       [Classical.safe_intro_global])]
         |> DatatypesData.put 
 	    (Symtab.update
 	     ((big_rec_name, dt_info), DatatypesData.get thy1)) 
         |> ConstructorsData.put