170 Datatype.add_datatype Datatype.default_config raw_dts thy |
170 Datatype.add_datatype Datatype.default_config raw_dts thy |
171 |
171 |
172 val lthy1 = Named_Target.theory_init thy1 |
172 val lthy1 = Named_Target.theory_init thy1 |
173 |
173 |
174 val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' |
174 val dtinfos = map (Datatype.the_info (Proof_Context.theory_of lthy1)) raw_full_dt_names' |
175 val {descr, sorts, ...} = hd dtinfos |
175 val {descr, ...} = hd dtinfos |
176 |
176 |
177 val raw_tys = Datatype_Aux.get_rec_types descr sorts |
177 val raw_tys = Datatype_Aux.get_rec_types descr |
178 val raw_ty_args = hd raw_tys |
178 val raw_ty_args = hd raw_tys |
179 |> snd o dest_Type |
179 |> snd o dest_Type |
180 |> map dest_TFree |
180 |> map dest_TFree |
181 |
181 |
182 val raw_cns_info = all_dtyp_constrs_types descr sorts |
182 val raw_cns_info = all_dtyp_constrs_types descr |
183 val raw_all_cns = (map o map) (fn (c, _, _, _) => c) raw_cns_info |
183 val raw_all_cns = (map o map) (fn (c, _, _, _) => c) raw_cns_info |
184 |
184 |
185 val raw_inject_thms = flat (map #inject dtinfos) |
185 val raw_inject_thms = flat (map #inject dtinfos) |
186 val raw_distinct_thms = flat (map #distinct dtinfos) |
186 val raw_distinct_thms = flat (map #distinct dtinfos) |
187 val raw_induct_thm = #induct (hd dtinfos) |
187 val raw_induct_thm = #induct (hd dtinfos) |