src/HOL/Tools/Datatype/datatype_abs_proofs.ML
changeset 33669 ae9a2ea9a989
parent 33643 b275f26a638b
child 33726 0878aecbf119
     1.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 13 17:15:35 2009 +0000
     1.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Fri Nov 13 19:57:46 2009 +0100
     1.3 @@ -156,9 +156,8 @@
     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 = "",
     1.8 -            alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true,
     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 = false, no_ind = true, skip_mono = true, fork_mono = false}
    1.12            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.13            (map dest_Free rec_fns)
    1.14            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []