src/HOL/Tools/inductive_realizer.ML
changeset 26535 66bca8a4079c
parent 26481 92e901171cc8
child 26626 c6231d64d264
--- a/src/HOL/Tools/inductive_realizer.ML	Thu Apr 03 17:54:19 2008 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Thu Apr 03 17:55:12 2008 +0200
@@ -351,7 +351,7 @@
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
         {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = "",
-          coind = false, no_elim = false, no_ind = false}
+          coind = false, no_elim = false, no_ind = false, skip_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Sign.base_name (name_of_thm intr), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))