> Some developer must have forgotten(!) to test the AFP when submitting a > change. My fault, sorry. I reverted the change (in HOL/Library/Word.thy) for now, since the consequences were bigger than I thought. Should really have tested better. Alex