[Hol-info] Type definitions: MosML bug?

[Michael N. <Mic...@ni...>]

Jens Brandt writes:
 
> Due to a bug in Moscow ML 2.00, it seems that new types cannot be
> created in HOL any more. All definitions throw an overflow
> exception:
 
> - new_type("s",0);
> ! Uncaught exception:
> ! Overflow
 
new_theory is also affected by this bug.  This means that most HOL
activity is completely impossible.  There's a straightforward
work-around that I have implemented and checked into the CVS
repository at SourceForge.  If you want an immediate fix, follow the
instructions for anonymous CVS access at

  http://sourceforge.net/cvs/?group_id=31790

and download the current working tree.  This works.  

For those (understandably) wary of having to use CVS, I hope that we
will produce either an easy-to-apply patch, or a release of
Kananaskis-2 in the very near future (i.e., within a week or two at
the most).

Regards,
Michael.