src/HOL/Tools/inductive_realizer.ML
changeset 33669 ae9a2ea9a989
parent 33666 e49bfeb0d822
child 33671 4b0f2599ed48
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 17:15:35 2009 +0000
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Fri Nov 13 19:57:46 2009 +0100
     1.3 @@ -351,8 +351,8 @@
     1.4  
     1.5      val (ind_info, thy3') = thy2 |>
     1.6        Inductive.add_inductive_global (serial ())
     1.7 -        {quiet_mode = false, verbose = false, kind = "", alt_name = Binding.empty,
     1.8 -          coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
     1.9 +        {quiet_mode = false, verbose = false, alt_name = Binding.empty, coind = false,
    1.10 +          no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    1.11          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.12            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),
    1.13             subst_atomic rlzpreds' (Logic.unvarify rintr)))