User-defined sorts cannot be referenced in quantified expressions

[mattulbrich]

Description

User-defined/Built-in KeY sorts are supposed to be accessible from within JML using a \dl_ escape. However, this does not work within quantified expressions.

Steps to reproduce

always

final class C {
	//@ invariant (\forall \dl_Seq c; c == c);
}

does not load in KeY.

--

• Commit: 7fe4e7d

[mattulbrich]

And they cannot be used in cast expressions either. (\dl_Seq)x reportedly tends to fail, too.