[isabelle-dev] AFP/Group-Ring-Module

[Tobias Nipkow]

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