(This comment is somewhat similar to Bug 1787.)

statEnv.namespace
    Judgments such as
        statEnv.namespace(NCName) = URI-or-#NULL-NAMESPACE
        statEnv.namespace(NCName) = URI
        fn:namespace-uri-from-QName(expanded-QName) = statEnv.namespace(Prefix)
    are malformed, as statEnv.namespace actually maps to a
        (namespace-kind, URI-or-#NULL-NAMESPACE)
    pair.

    The minimal change would be to forms such as:
        statEnv.namespace(NCName) = (NamespaceKind,URI-or-#NULL-NAMESPACE)
        etc
    where we don't care what gets bound to the NamespaceKind pattern.

    This affects:
        3.1.1.1 / Sem / rule 1 / premise 1
        3.1.1.1 / Sem / rule 3 / premise 1
        3.1.1.1 / Sem / rule 5 / premise 1
        3.1.1.1 / Sem / rule 7 / premise 1
        4.7.3.2 / DErr / rule 3 / premise 2
        8.2.3.1.1 / -- / rule 3 / premise 2
        8.2.3.1.1 / -- / rule 5 / premise 2
        8.2.3.1.1 / -- / rule 9 / premise 2
        8.2.3.1.1 / -- / rule 16 / premise 2
        8.2.3.1.1 / -- / rule 22 / premise 1
        8.2.3.2.1 / Sem / rule 1 / premise 3
        8.2.3.2.1 / Sem / rule 3 / premise 3
(leftover from last year, comments #014, 034, 035)

URI:
    There is no non-terminal named 'URI'.
    At one occurrence, 3.1.1 / -- / rule 1 / conclusion
        statEnv |- declare namespace NCName = URI Expr*
    it obviously should be changed to URILiteral, because that's what the
    EBNF dictates.

    In other cases, I think you intend 'URI' to mean, not a concrete
    syntactic literal, but rather an abstract value. One that's had a
    teensy bit of normalization applied (de-StringLiteral-ization and
    whitespace normalization). That is, a value in the value space of
    xs:anyURI. Or, in the Formal Value syntax, an 'AnyURI'.

    Thus, I think all other occurrences of 'URI' symbol (in judgments and
    accompanying prose) should be changed to 'AnyURI'.  This affects:
        3.1.1 /
        3.1.1.1 /
        4.1.2 /
        4.1.5 /
        4.7.3.1 /
        5.2 / Notation
        5.2 / Notation
        5.11 /

URILiteral:
    Moreover, 'URILiteral' often appears in contexts that want a value
    rather than a chunk of concrete syntax. Specifically, 'URILiteral'
    should be changed to 'AnyURI' in the following judgments:
        5.2 / SCP / rule 1 / conclusion
        5.2 / DCP / rule 1 / conclusion
        5.4 / SCP / rule 1 / premise 1
        5.5 / SCP / rule 1 / premise 1
        5.10 / SCP / rule 2 / premise 3
        5.10 / SCP / rule 3 / premise 3
        5.11 / SCP / rule 1 / premise (1|2|3)
        5.11 / DCP / rule 3 / premise (1|2|3)
        5.12 / SCP / rule 1 / premise 1
        5.13 / SCP / rule 2 / premise 2
        5.13 / SCP / rule 4 / premise 2

    In each of these rules, there is also one or more occurrences of
    'URILiteral' which *are* meant syntactically and should not be
    changed. To connect the latter to the former, you need to add a
    premise such as:
        URILiteral has literal value AnyURI