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