HOL
HOL copied to clipboard
Remove the use of `free_vars` in HO_PART_MATCH
https://github.com/HOL-Theorem-Prover/HOL/blob/24e40cd1c7f7e235a5c9f32f692c0d9ae04ddb2b/src/1/Drule.sml#L1802C1-L1804C71
HO_PART_MATCH calls free_vars. Term.free_vars is much slower than Term.FVL.
This might just be replacing free_vars bod with HOLset.listItems (FVL [bod]) if the order doesn't matter.
I'd be happy to receive a PR along these lines.