compsets should become functional

[mn200]

The references hidden inside compsets make manipulating them a pain. They also make concurrent operation hard.

[konrad-slind]

Agreed. I was never able to argue Bruno out of the ref. --Konrad.

On Fri, Nov 30, 2018 at 8:42 PM Michael Norrish [email protected] wrote:

The references hidden inside compsets make manipulating them a pain. They also make concurrent operation hard.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/620, or mute the thread https://github.com/notifications/unsubscribe-auth/ABDgD1iaEu7CJQ15dACL2L1hCD47B47eks5u0ex7gaJpZM4Y8rHq .