src/HOL/Tools/inductive_realizer.ML
changeset 26477 ecf06644f6cb
parent 26343 0dd2eab7b296
child 26481 92e901171cc8
--- a/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 13:03:07 2008 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Sat Mar 29 13:03:08 2008 +0100
@@ -350,7 +350,7 @@
 
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
-        {verbose = false, kind = Thm.theoremK, alt_name = "",
+        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = "",
           coind = false, no_elim = false, no_ind = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Sign.base_name (name_of_thm intr), []),