src/HOL/Tools/inductive_realizer.ML
changeset 31174 f1f1e9b53c81
parent 30722 623d4831c8cf
child 31177 c39994cb152a
     1.1 --- a/src/HOL/Tools/inductive_realizer.ML	Sat May 16 15:24:35 2009 +0200
     1.2 +++ b/src/HOL/Tools/inductive_realizer.ML	Sat May 16 20:17:59 2009 +0200
     1.3 @@ -349,7 +349,7 @@
     1.4  
     1.5      val (ind_info, thy3') = thy2 |>
     1.6        InductivePackage.add_inductive_global (serial_string ())
     1.7 -        {quiet_mode = false, verbose = false, kind = Thm.theoremK, alt_name = Binding.empty,
     1.8 +        {quiet_mode = false, verbose = false, kind = Thm.generated_theoremK, alt_name = Binding.empty,
     1.9            coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
    1.10          rlzpreds rlzparams (map (fn (rintr, intr) =>
    1.11            ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),