HOL icon indicating copy to clipboard operation
HOL copied to clipboard

Remove the use of `free_vars` in HO_PART_MATCH

Open ordinarymath opened this issue 4 months ago • 1 comments

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.

ordinarymath avatar Aug 21 '25 16:08 ordinarymath

I'd be happy to receive a PR along these lines.

mn200 avatar Aug 22 '25 03:08 mn200