Email Gateway (Aug 19 2022 at 08:43): Email Gateway (Aug 19 2022 at 08:43):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.
Email Gateway (Aug 19 2022 at 08:43):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: Apr 18 2024 at 04:17 UTC