153 |> Inductive.add_inductive_global |
153 |> Inductive.add_inductive_global |
154 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name', |
154 {quiet_mode = #quiet config, verbose = false, alt_name = Binding.name big_rec_name', |
155 coind = false, no_elim = false, no_ind = true, skip_mono = true} |
155 coind = false, no_elim = false, no_ind = true, skip_mono = true} |
156 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) |
156 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) |
157 (map dest_Free rec_fns) |
157 (map dest_Free rec_fns) |
158 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] |
158 (map (fn x => (Binding.empty_atts, x)) rec_intr_ts) [] |
159 ||> Sign.restore_naming thy0; |
159 ||> Sign.restore_naming thy0; |
160 |
160 |
161 (* prove uniqueness and termination of primrec combinators *) |
161 (* prove uniqueness and termination of primrec combinators *) |
162 |
162 |
163 val _ = Old_Datatype_Aux.message config |
163 val _ = Old_Datatype_Aux.message config |