[isabelle-dev] [isabelle] normalization method introduces schematic type variables in HOL/Word types

[Andreas Lochbihler]

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
>