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

[Jasmin Christian Blanchette]

Hi again,

> 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

Update: The same problem occurs already with revision 6975db7fd6f0, i.e. it has nothing to do with my recent changes to the "metis" proof method and is apparently unrelated to the AFP failure. To reproduce it, fire up Proof General with the HOL image and process

    theory Scratch
    imports Main
    begin

    lemma "a : {x. P x} ==> P a"
    proof -
      assume "a : {x. P x}"
      hence "a : P" apply (metis Collect_def) done

The disturbing error message should appear on the "done".

When it comes to the AFP failure, there's a second AFP failure, in JinjaThreads, that's obviously related to the servers' being down yesterday; the Lam-ml-Normalization failure could be due to that, too. Lukas is helping find out.

Jasmin