[isabelle-dev] datatype_new problem

[Christian Sternagel]

Dear Jasmin,

consider the following datatype specification

   datatype_new 'f f =
     F1 'f 'f 'f 'f |
     F2 'f 'f 'f 'f

(which takes about 1 second with Isabelle2014-RC0) does not terminate 
within a few minutes anymore.

Note that this is a minimal example that originates from IsaFoR

http://cl2-informatik.uibk.ac.at/rewriting/mercurial.cgi/IsaFoR/file/2a9fc552f074/IsaFoR/Nonloop_SRS_Impl.thy#l214

and does not terminate within 10 hours on Cezary's machine.

I did not have time to do a proper bisect until now. Maybe you could 
have a look ;)

cheers

chris