equal
deleted
inserted
replaced
939 ||>> mk_Frees "R" pred2RTs |
939 ||>> mk_Frees "R" pred2RTs |
940 ||>> mk_Frees "S" pred2RTsBsCs |
940 ||>> mk_Frees "S" pred2RTsBsCs |
941 ||>> mk_Frees "R" transfer_domRTs |
941 ||>> mk_Frees "R" transfer_domRTs |
942 ||>> mk_Frees "S" transfer_ranRTs; |
942 ||>> mk_Frees "S" transfer_ranRTs; |
943 |
943 |
944 val fs_copy = map2 (retype_free o fastype_of) fs gs; |
944 val fs_copy = map2 (retype_const_or_free o fastype_of) fs gs; |
945 val x_copy = retype_free CA' y; |
945 val x_copy = retype_const_or_free CA' y; |
946 |
946 |
947 val rel = mk_bnf_rel pred2RTs CA' CB'; |
947 val rel = mk_bnf_rel pred2RTs CA' CB'; |
948 val relAsAs = mk_bnf_rel self_pred2RTs CA' CA'; |
948 val relAsAs = mk_bnf_rel self_pred2RTs CA' CA'; |
949 val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; |
949 val bnf_wit_As = map (apsnd (mk_bnf_t As')) bnf_wits; |
950 |
950 |