src/HOL/Tools/inductive_realizer.ML
changeset 29389 0a49f940d729
parent 29281 b22ccb3998db
child 29579 cb520b766e00
--- a/src/HOL/Tools/inductive_realizer.ML	Wed Jan 07 23:52:18 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML	Wed Jan 07 23:53:08 2009 +0100
@@ -347,7 +347,7 @@
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
         {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
-          coind = false, no_elim = false, no_ind = false, skip_mono = false}
+          coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Sign.base_name (name_of_thm intr)), []),
            subst_atomic rlzpreds' (Logic.unvarify rintr)))