[Hol-developers] PSL proof fails

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

I realised that I hadn't checked my latest change (yesterday's change
to the simplifier's mk_rewrites code) against the PSL example.  I've
just done this this morning, and it fails to prove a lemma 

  boolean_safety_violation 

in ExecutableSemanticsScript.sml.

I don't think this failure is my fault though because the same error
arises when I try to run the example through a version of HOL without
the change to mk_rewrites in place.

Of course, it may well be that the error arises because of some
earlier change I made to the system.  I will endeavour to check all
the examples when I make any future changes.  (This is relatively easy
to do using the build_examples script from <holdir>/developers/ )

Michael.