[isabelle] ML code in Isar files

Using the latest development version of Isabelle,
I have Isar files thus:


ML {*

val _ = bind_thms ("word_arith_nat_defs", map dop fas2) ;


 ... =   ... word_arith_nat_defs ...


Now when the semicolon in the above is omitted, the code fails with a message

Value or constructor (word_arith_nat_defs) has not been declared

When the semicolon is replaced the code works fine.

Can anyone tell why this is?


Jeremy Dawson

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