Re: [isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
On Mon, 23 Feb 2015, Joachim Breitner wrote:
what is usually the cause for the error message
*** exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop
To reproduce with Isabelle-2014, run
$ git clone https://github.com/gattschardo/open-inductive
$ cd open-inductive
add "Open_Arith_Eval" to "theories" in ROOT
$ isabelle build -D .
It does not (seem to) occur in Isabelle/jEdit.
The parallelism is less aggressive in interactive PIDE document processing
than in batch build. This might be a reason for the breakdown of the
forked proof, see als src/Pure/thm.ML function future_result.
Since I can't reproduce the problem, I recommend to insert a different
exception there, e.g. TERM with the relevant arguments for more
Skimming over the sources of open_inductive.ML, there are various points
that look a bit suspicious concerning hyps and context, which might be a
source of such problems. Occasionally it looks like the abstract notion
of goal state -- which happens to be represented as concrete thm, but with
certain implicit policies -- is not properly observed.
I have more to say about the sources, but that has to wait.
This archive was generated by a fusion of
Pipermail (Mailman edition) and