Re: [isabelle] exception Option
On 05.09.2012 14:16, Henri.Debrat at loria.fr wrote:
Does anyone know what I should do when encountering the following error:
exception Option raised (line 81 of "General/basics.ML")
This is an internal error and as such shouldn't reach the user. Without
knowing the exact situation, it is hard to see, where this issue stems from.
I was using proof (auto dest: ext[OF _ _]) in case it might help.
Can you give an complete minimal example (i.e. a complete theory file)?
Also, which version of Isabelle are you using?
This archive was generated by a fusion of
Pipermail (Mailman edition) and