Re: [isabelle] Exception: THM 0 raised in thm.ML when defining function

Hi Dominic,

> I have a fairly large recursive function (~160 lines) that is causing
> problems, in when I try to get Isabelle to accept the function
> definition (using either the fun or function keyword) I am getting the
> following output:
>   * exception THM 0 raised (line 705 of "thm.ML"):
>   * implies_elim: major premise
> followed by what looks like a lengthy internal proof state of some
> sort from the function package.  I have stepped through the function
> commenting out chunks of code and putting "undefined" everywhere, and
> it appears that the problem is in the final recursive call at the
> bottom of my definition.
> How can I work around this other than trying to split my function up,
> or begin to try to find out what the problem is?  The error message is
> not very helpful in working out where the problem lies.  Is there a
> known common cause for this exception when defining functions?

I think the best what can be done at the moment is to provide a minimal
example here on the mailing list.

All the best,


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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