522 xtor_co_induct = xtor_co_induct_thm, |
522 xtor_co_induct = xtor_co_induct_thm, |
523 dtor_ctors = of_fp_res #dtor_ctors (*too general types*), |
523 dtor_ctors = of_fp_res #dtor_ctors (*too general types*), |
524 ctor_dtors = of_fp_res #ctor_dtors (*too general types*), |
524 ctor_dtors = of_fp_res #ctor_dtors (*too general types*), |
525 ctor_injects = of_fp_res #ctor_injects (*too general types*), |
525 ctor_injects = of_fp_res #ctor_injects (*too general types*), |
526 dtor_injects = of_fp_res #dtor_injects (*too general types*), |
526 dtor_injects = of_fp_res #dtor_injects (*too general types*), |
527 xtor_maps = of_fp_res #xtor_maps (*too general types and terms*), xtor_map_uniques = [], |
527 xtor_maps = of_fp_res #xtor_maps (*too general types and terms*), |
|
528 xtor_map_unique = TrueI (*wrong*), |
528 xtor_setss = of_fp_res #xtor_setss (*too general types and terms*), |
529 xtor_setss = of_fp_res #xtor_setss (*too general types and terms*), |
529 xtor_rels = of_fp_res #xtor_rels (*too general types and terms*), |
530 xtor_rels = of_fp_res #xtor_rels (*too general types and terms*), |
530 xtor_un_fold_thms_legacy = xtor_co_rec_thms (*wrong*), |
531 xtor_un_fold_thms_legacy = xtor_co_rec_thms (*wrong*), |
531 xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*), |
532 xtor_co_rec_thms = xtor_co_rec_thms (*too general types and terms*), |
532 xtor_un_fold_uniques_legacy = [], xtor_co_rec_uniques = [], |
533 xtor_un_fold_unique_legacy = TrueI (*too general types and terms*), |
|
534 xtor_co_rec_unique = TrueI (*wrong*), |
533 xtor_un_fold_o_maps_legacy = fp_rec_o_maps (*wrong*), |
535 xtor_un_fold_o_maps_legacy = fp_rec_o_maps (*wrong*), |
534 xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*), |
536 xtor_co_rec_o_maps = fp_rec_o_maps (*theorems about old constants*), |
535 xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [], |
537 xtor_un_fold_transfers_legacy = [], xtor_co_rec_transfers = [], |
536 xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []} |
538 xtor_rel_co_induct = xtor_rel_co_induct, dtor_set_inducts = []} |
537 |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); |
539 |> morph_fp_result (Morphism.term_morphism "BNF" (singleton (Variable.polymorphic lthy)))); |