Re: [isabelle] normalization method introduces schematic type variables in HOL/Word types



Hi Florian,

Thanks for looking into this.

On 25/06/13 20:12, Florian Haftmann wrote:
An even more minimal example:

theory Foo
imports "~~/src/HOL/Word/Word"
begin

definition
   "example = (1 + 1 :: 4 word)"

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.

Andreas




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