Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP

Hi Lars & Fabian,

> I have recently seen this behavior as well (in Isabelle2014-RC1) and can reproduce it as follows (it seems important that mashine learning is "finished"):
> theory Scratch imports Main begin
> lemma True sledgehammer learn_isar by (rule TrueI)
> notepad begin
> fix P
> have "P"
>   by nothing
> have "P"
>   (* invoke s/h here *)
> inserting a textual "sledgehammer" or "sledgehammer learn_isar" command shows nothing in the output, but colors the command in red.

Thank you for your report! The attached changeset for "isabelle-release" fixes it. In short, it's naive to expect "Thm.proof_body_of" never to throw any exceptions.

Makarius: Could you apply the attached changeset to "isabelle-release"? Thanks.


Attachment: try_proof_body
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.