It is a matter of ongoing discussion how much type information we
require from the user for the sake of readability of specification.
Since types of quantified variables are important part of axioms
and lemmas, we required them for the same reason we require the
full prototypes for functions and predicates. However, when we
typecheck program annotations, explicit types in quantifiers may
quickly become an annoyance. Let's say, we define a polymorphic
function "fn":

  let fn x y
    requires { forall z:'a. ... -> z = x }
  = ...

Since in programs we [are going to] accept implicit type variables,
the user may omit the types of "x" and "y", and they will be inferred
by the typechecker. Now, if we are obliged to write the type of "z"
in the postcondition, we cannot simply write 'a, because it will not
unify with the implicit type of "x" (remember that programs are typed
independently of specs). So, if we write the type of "z", we also have
to write the type of "x". This is annoying and may even lead to errors
if, by mistake, the user chooses 'a for the type of "x" and thus
freezes 'a in all function definitions in "fn" while they were
polymorphic in 'a till then.

For this reason, it seems reasonable to accept untyped variables
under quantifiers (DISCUSS: should we accept them only in specs?).
However, we still require type variables in logic to be explicitly
named (unless they come from the program, then they are accepted),
and thus polymorphic axioms and lemmas would still have to have
the explicitly typed quantified variables.