src/HOL/Tools/Datatype/datatype_rep_proofs.ML
changeset 33669 ae9a2ea9a989
parent 33643 b275f26a638b
child 33726 0878aecbf119
     1.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Nov 13 17:15:35 2009 +0000
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Fri Nov 13 19:57:46 2009 +0100
     1.3 @@ -175,9 +175,8 @@
     1.4        thy1
     1.5        |> Sign.map_naming Name_Space.conceal
     1.6        |> Inductive.add_inductive_global (serial ())
     1.7 -          {quiet_mode = #quiet config, verbose = false, kind = "",
     1.8 -           alt_name = Binding.name big_rec_name, coind = false, no_elim = true, no_ind = false,
     1.9 -           skip_mono = true, fork_mono = false}
    1.10 +          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    1.11 +           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
    1.12            (map (fn s => ((Binding.name s, UnivT'), NoSyn)) rep_set_names') []
    1.13            (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    1.14        ||> Sign.restore_naming thy1