src/HOL/Tools/function_package/inductive_wrap.ML

--- a/src/HOL/Tools/function_package/inductive_wrap.ML	Fri Mar 28 22:39:47 2008 +0100
+++ b/src/HOL/Tools/function_package/inductive_wrap.ML	Sat Mar 29 13:03:05 2008 +0100
@@ -41,7 +41,8 @@
     let
       val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
           InductivePackage.add_inductive_i
-            {verbose = ! Toplevel.debug,
+            {quiet_mode = false,
+              verbose = ! Toplevel.debug,
               kind = Thm.internalK,
               alt_name = "",
               coind = false,