HOL-Theorem-Prover
Implement listener for term matching
It would nice to have a listener module for term matching that can be turned on and off. The first order matcher in Term.sml wastes time in calling KernelSig.id_toString https://github.com/HOL-Theorem-Prover/HOL/blob/9a0aad85ccaf911c3b43823532a691042a0f879d/src/0/Term.sml#L909-L910 and concatenating the resulting string. The higher order matcher doesn't give good error messages but wastes alot of time in wrapping the error messages using wrap_exn. https://github.com/HOL-Theorem-Prover/HOL/blob/9a0aad85ccaf911c3b43823532a691042a0f879d/src/postkernel/HolKernel.sml#L759-L763 The reason I'm doing it this way is I can't figure out a way to print lazy errors in mosml and I think @digama0 also prefers listener over errors.
