I tried changing a few occurrences to use diag_string instead (see patch) and this seemed to solve the issue this those cases.
A more interesting example is use_string "plus_conv %SZT%Q%>%;";The patch reduces the number of Qs in the exception message from 16 to 4 but would we expect the 4 Qs to reduce to 1? As ordinary users _must_ be aware that Q in a string is escaped as QQQQ, perhaps not?
Description: GNU Zip compressed data
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com