src/HOL/Nominal/nominal_datatype.ML
changeset 33669 ae9a2ea9a989
parent 33643 b275f26a638b
child 33726 0878aecbf119
     1.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 13 17:15:35 2009 +0000
     1.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Fri Nov 13 19:57:46 2009 +0100
     1.3 @@ -569,9 +569,8 @@
     1.4        thy3
     1.5        |> Sign.map_naming Name_Space.conceal
     1.6        |> Inductive.add_inductive_global (serial ())
     1.7 -          {quiet_mode = false, verbose = false, kind = "",
     1.8 -           alt_name = Binding.name big_rep_name, coind = false, no_elim = true, no_ind = false,
     1.9 -           skip_mono = true, fork_mono = false}
    1.10 +          {quiet_mode = false, verbose = false, alt_name = Binding.name big_rep_name,
    1.11 +           coind = false, no_elim = true, no_ind = false, skip_mono = true, fork_mono = false}
    1.12            (map (fn (s, T) => ((Binding.name s, T --> HOLogic.boolT), NoSyn))
    1.13               (rep_set_names' ~~ recTs'))
    1.14            [] (map (fn x => (Attrib.empty_binding, x)) intr_ts) []
    1.15 @@ -1513,9 +1512,8 @@
    1.16        thy10
    1.17        |> Sign.map_naming Name_Space.conceal
    1.18        |> Inductive.add_inductive_global (serial ())
    1.19 -          {quiet_mode = #quiet config, verbose = false, kind = "",
    1.20 -           alt_name = Binding.name big_rec_name, coind = false, no_elim = false, no_ind = false,
    1.21 -           skip_mono = true, fork_mono = false}
    1.22 +          {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name,
    1.23 +           coind = false, no_elim = false, no_ind = false, skip_mono = true, fork_mono = false}
    1.24            (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts))
    1.25            (map dest_Free rec_fns)
    1.26            (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) []