src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33643 b275f26a638b
parent 33459 a4a38ed813f7
child 33669 ae9a2ea9a989
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 12 21:59:35 2009 +0100
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Thu Nov 12 22:02:11 2009 +0100
     1.3 @@ -156,7 +156,7 @@
     1.4        thy0
     1.5        |> Sign.map_naming Name_Space.conceal
     1.6        |> Inductive.add_inductive_global (serial ())
     1.7 -          {quiet_mode = #quiet config, verbose = false, kind = Thm.internalK,
     1.8 +          {quiet_mode = #quiet config, verbose = false, kind = "",
     1.9              alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
    1.10              skip_mono = true, fork_mono = false}
    1.11            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))