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