# HG changeset patch
# User berghofe
# Date 935595201 -7200
# Node ID 228b711ad68c6d8bd082ae695dfd765fe184fade
# Parent  3e91b07223ad6836fab504f9856f815745a1c910
Removed "Adding axioms ..." message.

diff -r 3e91b07223ad -r 228b711ad68c 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);