Removed "Adding axioms ..." message.
authorberghofe
Wed, 25 Aug 1999 17:33:21 +0200
changeset 7349 228b711ad68c
parent 7348 3e91b07223ad
child 7350 708bd83745c5
Removed "Adding axioms ..." message.
src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Wed Aug 25 17:11:42 1999 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Wed Aug 25 17:33:21 1999 +0200
@@ -636,9 +636,6 @@
 fun add_ind_axm verbose declare_consts alt_name coind no_elim no_ind cs
     atts intros monos con_defs thy params paramTs cTs cnames =
   let
-    val _ = if verbose then message ("Adding axioms for " ^ coind_prefix coind ^
-      "inductive set(s) " ^ commas_quote cnames) else ();
-
     val rec_name = if alt_name = "" then space_implode "_" cnames else alt_name;
 
     val ((intr_names, intr_ts), intr_atts) = apfst split_list (split_list intros);