[isabelle] exception THM 0 raised (line 532 of "thm.ML"): future_result: bad prop



Dear list,

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.

Thanks,
Joachim


-- 
Dipl.-Math. Dipl.-Inform. Joachim Breitner
Wissenschaftlicher Mitarbeiter
http://pp.ipd.kit.edu/~breitner

Attachment: signature.asc
Description: This is a digitally signed message part



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