On 19/07/18 13:42, Tobias Nipkow wrote:
> I have the same problem, and on my machine it is reproduceable (and it
> did not go away over the past week, although I tried different versions
> of the devel repository).

I suspect that it is a deferred error due to lazy facts in locale
interpretation.

In Isabelle/5820f0f379ae, I have now added the system option
"strict_facts" to avoid this.

You can use it with "isabelle build -o strict_facts" or add it
temporarily to $ISABELLE_HOME_USER/etc/preferences as "strict_facts =
true" (notably for "isabelle jedit").


        Makarius

_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to