4.1.5 Function calls
Comments on the definition of [Expr]AtomizeAtomic(SequenceType):

a) In the first case, where the result if fn:data(Expr),
you have the judgment Expr:Type.  I think you mean
statEnv |- Expr:Type, since type inferencing always occurs in
the context of the static environment group.

b) The exclusion "and not (Type=empty)" is unnecessary since there
is no harm in invoking fn:data(()).  The parameter type of
fn:data() is item()* so it is already defined on the empty
sequence.

c) The variable Type is a free variable with no quantification.
You cannot mean universal quantification, since 
(for all Type)(statEnv |- Expr:Type) can never be true.
You must mean (there exists Type)[Expr:Type and not (Type=empty)].

d) Instead of "Expr : Type and not (Type = empty)", you could
just write "not (Expr : empty)", which has the advantage of
eliminating the variable Type.

e) The judgment 
SequenceType <: xdt:anyAtomicType* is not defined because the 
<: relationship holds between two Types.  You need to first
transform the SequenceType into its equivalent Type and then
you can test this relationship.  Thus the condition is
[SequenceType]sequencetype <: xdt:anyAtomicType*

f) The definition will read better if you place the "if" clause
around the rule rather than nested within it.

The summary of this analysis is that the rule is better
expressed:

If [SequenceType]sequencetype <: xdt:anyAtomicType* 
then fn:data(Expr)
else Expr