[isabelle-dev] Fwd: status (AFP)

[Brian Huffman]

On Sun, Sep 18, 2011 at 1:42 AM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
> After not running in the test for quite some time, JinjaThreads now comes back failing:
>
> *** Undeclared constant: "semilattice_sup_class.sup"
> *** At command "definition" (line 20 of "/home/kleing/afp/devel/thys/JinjaThreads/Execute/Cset_without_equal.thy")
> val it = (): unit
> Exception- TOPLEVEL_ERROR raised
> *** ML error
>
> It looks like something in the class setup changed slightly. Could somebody who is more up-to-date in this area have a look, please?

This must be due to the recent changeset:

added syntactic classes for "inf" and "sup"
http://isabelle.in.tum.de/repos/isabelle/rev/5e51075cbd97

The fix is probably to replace "semilattice_sup_class.sup" with "sup_class.sup".

- Brian