src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33643 b275f26a638b
parent 33459 a4a38ed813f7
child 33669 ae9a2ea9a989
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 12 21:59:35 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 12 22:02:11 2009 +0100
@@ -156,7 +156,7 @@
       thy0
       |> 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 = true,
             skip_mono = true, fork_mono = false}
           (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))