# HG changeset patch
# User wenzelm
# Date 928505871 -7200
# Node ID 34270fe45516eefd87e40109ce640b9c2f006e78
# Parent  6eba3d69037b2a381f301a5e756ebf888de82c94
no message "Adding axioms for datatype(s)";

diff -r 6eba3d69037b -r 34270fe45516 src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Fri Jun 04 16:17:20 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Fri Jun 04 16:17:51 1999 +0200
@@ -275,8 +275,6 @@
     val used = foldr add_typ_tfree_names (recTs, []);
     val newTs = take (length (hd descr), recTs);
 
-    val _ = message ("Adding axioms for datatype(s) " ^ commas_quote new_type_names);
-
     (**** declare new types and constants ****)
 
     val tyvars = map (fn (_, (_, Ts, _)) => map dest_DtTFree Ts) (hd descr);