Remove duplicate mllist mapPartial definition

[mah1104ahm]

Summary

• remove the duplicate mapPartial definition from mllist
• prove the existing mapPartial_thm against listTheory.mapPartial_def
• leave the public theorem available to downstream scripts

Verification

• confirmed basis/pure/mllistScript.sml no longer defines mapPartial
• git diff --check
• full HOL build not run locally because Holmake is unavailable

Closes #1449

[tanyongkiam]

Hi, thanks for the contribution.

I think the PR should be done more carefully and with HOL used (at least checking the files that were touched).

For example, there still remains references to mllistTheory.mapPartial_def.

[mah1104ahm]

Thank you for the review. You are right: the original change was not sufficiently verified with HOL. I found and corrected the three remaining mllistTheory.mapPartial_def references in holModelConservativityScript.sml locally. I also inspected regression job 3495: it fails earlier in holExtensionTheory at abs_or_rep_matches_type_matches, so fixing those references alone is not enough to claim a working patch. I do not currently have a working HOL/PolyML environment available locally. I am holding the follow-up push until the affected theories can be checked, rather than presenting the textual corrections as proof validation. Thank you for identifying the gap. M Ahmed