When I run AFP/Group-Ring-Module, it fails: *** empty result sequence -- proof command failed *** At command "apply" (line 6032 of "/mnt/home/nipkow/AFP/afp-devel/thys/Group-Ring-Module/Algebra1.thy").
I don't think this is caused by my own change but must have been there for a couple of days. (It seems like the daily AFP test is not working at the moment.) I looked at the problem and it appears that the ALL/--> structure of a formula after simplification with *locale* stuff has changed.... Tobias
