[isabelle-dev] Stymied by cryptic failure in Product_type.thy

[Josh Tilles]

On Feb 18, 2014, at 2:19 AM, Lars Noschinski <noschinl at in.tum.de> wrote:

> The position of the error message is a bit misleading. It is not the qed which fails. Instead, after finishing the proof, the free_constructors command tries to prove something on its own -- and fails.

Aha! That’s exactly what I needed to know. There was a line in ctr_sugar_tactics.ML that contained `claset_of @{theory_context IHOL}`; changing `IHOL` to `CHOL` let everything else (through Complex_Main) compile.

Thank you Lars!

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 496 bytes
Desc: Message signed with OpenPGP using GPGMail
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20140221/31917d1f/attachment.sig>