153 |
153 |
154 val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) = |
154 val ({intrs = rec_intrs, elims = rec_elims, ...}, thy1) = |
155 InductivePackage.add_inductive_global (serial_string ()) |
155 InductivePackage.add_inductive_global (serial_string ()) |
156 {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, |
156 {quiet_mode = ! quiet_mode, verbose = false, kind = Thm.internalK, |
157 alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true, |
157 alt_name = Binding.name big_rec_name', coind = false, no_elim = false, no_ind = true, |
158 skip_mono = true} |
158 skip_mono = true, fork_mono = false} |
159 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) |
159 (map (fn (s, T) => ((Binding.name s, T), NoSyn)) (rec_set_names' ~~ rec_set_Ts)) |
160 (map dest_Free rec_fns) |
160 (map dest_Free rec_fns) |
161 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0; |
161 (map (fn x => (Attrib.empty_binding, x)) rec_intr_ts) [] thy0; |
162 |
162 |
163 (* prove uniqueness and termination of primrec combinators *) |
163 (* prove uniqueness and termination of primrec combinators *) |