  From the viewpoint of the theory of orthomodular lattices of elementary
propositions, Quantum Theories can be formulated in real, complex or
quaternionic Hilbert spaces as established in Sol\'er's theorem. The said
lattice eventually coincides with the lattice of all orthogonal projectors on a
separable Hilbert space over R, C, or over the algebra of quaternions H.
Quantum states are $\sigma$-additive probability measures on that non-Boolean
lattice. Gleason's theorem proves that, if the Hilbert space is separable with
dimension >2 and the Hilbert space is either real or complex, then states are
one-to-one with standard density matrices (self-adjoint, positive, unit-trace,
trace-class operators). The extension of this result to quaternionic Hilbert
spaces was obtained by Varadarajan in 1968. Unfortunately, even if the hard
part of the proof is correct, the formulation of this extension is
mathematically incorrect. This is due to some peculiarities of the notion of
trace in quaternionic Hilbert spaces, e.g., basis dependence, making the theory
of trace-class operators in quaternionic Hilbert spaces different from the
standard theory in real and complex Hilbert spaces. A minor issue also affects
Varadarajan's statement for real Hilbert space formulation. This paper is
mainly devoted to present Gleason-Varadarajan's theorem into a technically
correct form valid for the three types of Hilbert spaces. After having develped
part of the general mathematical technology of trace-class operators in
(generally non-separable) quaternionic Hilbert spaces, we prove that only the
{\em real part} of the trace enters the formalism of quantum theories (also
dealing with unbounded observables and symmetries) and it can be safely used to
formulate and prove a common statement of Gleason's theorem.
