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



Hi,

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?

Many thanks,
Dominic




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