The Axiom of Choice has been implemented. To turn it on, load LISPM2;CHOICE QFASL. Enabling this axiom will allow some programs to be greatly simplified, but may make others impossible, so be warned. Work on GCH is continuing but don't expect anything for a few more months.