311 |> add_dummies (Datatype.add_datatype {strict = false, quiet = false}) |
311 |> add_dummies (Datatype.add_datatype {strict = false, quiet = false}) |
312 (map (pair false) dts) [] |
312 (map (pair false) dts) [] |
313 ||> Extraction.add_typeof_eqns_i ty_eqs |
313 ||> Extraction.add_typeof_eqns_i ty_eqs |
314 ||> Extraction.add_realizes_eqns_i rlz_eqs; |
314 ||> Extraction.add_realizes_eqns_i rlz_eqs; |
315 val dt_names = these some_dt_names; |
315 val dt_names = these some_dt_names; |
316 val case_thms = map (#case_rewrites o Datatype.the_info thy2) dt_names; |
316 val case_thms = map (#case_rewrites o Datatype_Data.the_info thy2) dt_names; |
317 val rec_thms = |
317 val rec_thms = |
318 if null dt_names then [] |
318 if null dt_names then [] |
319 else #rec_rewrites (Datatype.the_info thy2 (hd dt_names)); |
319 else #rec_rewrites (Datatype_Data.the_info thy2 (hd dt_names)); |
320 val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o |
320 val rec_names = distinct (op =) (map (fst o dest_Const o head_of o fst o |
321 HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms); |
321 HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) rec_thms); |
322 val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) => |
322 val (constrss, _) = fold_map (fn (s, rs) => fn (recs, dummies) => |
323 if member (op =) rsets s then |
323 if member (op =) rsets s then |
324 let |
324 let |