--- a/src/ZF/Tools/datatype_package.ML Thu Jan 13 17:31:30 2000 +0100
+++ b/src/ZF/Tools/datatype_package.ML Thu Jan 13 17:34:39 2000 +0100
@@ -392,7 +392,9 @@
(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