[isabelle-dev] AFP failure in Lam-ml-Normalization

[Jasmin Blanchette]

Hi all,

Somewhere between 43ca06e6c168 and 6975db7fd6f0, I seem to have broken the AFP entry "Lam-ml-Normalization". However, I cannot reproduce the problem on my machine -- whether in Proof General nor using "isabelle make".

On the other hand, I do get the following disturbing messages in Proof General:

    Exception trace for exception - UNDEF raised in Isar/toplevel.ML line 494

    Toplevel.end_proof(1)(1)(1)
    End of trace

    Exception trace for exception - UNDEF raised in Isar/toplevel.ML line 457

    Toplevel.end_local_theory-(1)(1)
    End of trace

If anybody has a clue about what's going on, please say so. In any case, I will continue investigating.

Thanks,

Jasmin