--- a/src/HOL/Tools/inductive_realizer.ML Fri Nov 13 15:48:52 2009 +0100
+++ b/src/HOL/Tools/inductive_realizer.ML Fri Nov 13 17:25:09 2009 +0100
@@ -351,7 +351,7 @@
val (ind_info, thy3') = thy2 |>
Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = Thm.generatedK, alt_name = Binding.empty,
+ {quiet_mode = false, verbose = false, kind = "", 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)), []),