# HG changeset patch
# User paulson
# Date 947781279 -3600
# Node ID fe7d6fd68ea3c715655fa7358ec795f361ba46d7
# Parent  a71686059be0e529b8ed7c9ae18ad5108cece610
change in add_thmss to suppress warning

diff -r a71686059be0 -r fe7d6fd68ea3 src/ZF/Tools/datatype_package.ML
--- 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