--- a/src/HOL/Nominal/nominal_datatype.ML Thu Nov 12 21:59:35 2009 +0100
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Nov 12 22:02:11 2009 +0100
@@ -569,7 +569,7 @@
thy3
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = false, verbose = false, kind = Thm.internalK,
+ {quiet_mode = false, verbose = false, kind = "",
alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
@@ -1513,7 +1513,7 @@
thy10
|> Sign.map_naming Name_Space.conceal
|> Inductive.add_inductive_global (serial ())
- {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
+ {quiet_mode = #quiet config, verbose = false, kind = "",
alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
skip_mono = true, fork_mono = false}
(map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))