From: Henri.Debrat@loria.fr
Hi,
Does anyone know what I should do when encountering the following error:
exception Option raised (line 81 of "General/basics.ML")
I was using proof (auto dest: ext[OF _ _]) in case it might help.
Henri.
From: Lars Noschinski <noschinl@in.tum.de>
Hi,
On 05.09.2012 14:16, Henri.Debrat@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?
-- Lars
Last updated: Nov 21 2024 at 12:39 UTC