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,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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