src/HOL/Tools/inductive_realizer.ML
changeset 31177 c39994cb152a
parent 31174 f1f1e9b53c81
child 31458 b1cf26f2919b
--- a/src/HOL/Tools/inductive_realizer.ML	Sun May 17 07:17:39 2009 +0200
+++ b/src/HOL/Tools/inductive_realizer.ML	Mon May 18 09:48:06 2009 +0200
@@ -349,7 +349,7 @@
 
     val (ind_info, thy3') = thy2 |>
       InductivePackage.add_inductive_global (serial_string ())
-        {quiet_mode = false, verbose = false, kind = Thm.generated_theoremK, alt_name = Binding.empty,
+        {quiet_mode = false, verbose = false, kind = Thm.generatedK, alt_name = Binding.empty,
           coind = false, no_elim = false, no_ind = false, skip_mono = false, fork_mono = false}
         rlzpreds rlzparams (map (fn (rintr, intr) =>
           ((Binding.name (Long_Name.base_name (name_of_thm intr)), []),