Florian has suggested making sledgehammer available earlier in the construction of Main, before PreList at least. This could be useful to developers. However, it requires Hilbert_Choice, which must also be introduced earlier. We previously put some effort into making virtually all of HOL independent of the axiom of choice, so this would be a reversal. However, I don't know of anybody who has actually taken advantage of the AC-free part; in particular, I don't think that the use of nominal methods requires this any more. Can anybody comment?
Larry
