Re: [isabelle] exception Option


On 05.09.2012 14:16, Henri.Debrat at 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?

  -- Lars

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