153 (descr' ~~ recTs ~~ rec_sets') ([], 0); |
153 (descr' ~~ recTs ~~ rec_sets') ([], 0); |
154 |
154 |
155 val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) = |
155 val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) = |
156 thy0 |
156 thy0 |
157 |> Sign.map_naming Name_Space.conceal |
157 |> Sign.map_naming Name_Space.conceal |
158 |> Inductive.add_inductive_global (serial ()) |
158 |> Inductive.add_inductive_global |
159 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name', |
159 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name', |
160 coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false} |
160 coind = false, no_elim = false, no_ind = true, skip_mono = true, fork_mono = false} |
161 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) |
161 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) |
162 (map dest_Free rec_fns) |
162 (map dest_Free rec_fns) |
163 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] |
163 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] |