Hi Florian,
Thanks a lot for fixing this. It now works like a charm.
Andreas
On 29/06/13 08:34, Florian Haftmann wrote:
Hi Andreas,
ML {* Code_Simp.dynamic_value @{theory} @{term example} *}
ML {* Nbe.dynamic_value @{theory} @{term example} *}
The last line just raises Option (line 81 of General/basics.ML). I got
these exceptions quite often, but I thought that I had just done
something wrong.
see now http://isabelle.in.tum.de/reports/Isabelle/rev/a2407f62a29f and
http://isabelle.in.tum.de/reports/Isabelle/rev/9c7f760d06c2.
Florian
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
