Re: [isabelle] 2014-RC1 issues: unify_trace_failure

On Mon, 4 Aug 2014, Lars Noschinski wrote:

Even when declared inside a global context, the attribute
unify_trace_failure emits the warning

   Ignoring local change of global option "unify_trace_failure"

two times. Reproduce with:

theory Scratch imports Pure begin

declare [[unify_trace_failure]]


Thanks for looking after such details. I have made 2-3 rounds over critical spots where warnings get emitted, and reduced the redundancy for the next release candidate.


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