Record package's "forall" theorem is wrong for polymorphic records

[mn200]

In particular, given a definition such as

Datatype:  rcd = <| fld1 : 'a -> num; fld2 : bool |>
End

The FORALL_rcd theorem uses an unnecessarily polymorphic fld1_fupdate function, giving:

> theorem "FORALL_rcd";
val it = ⊢ ∀P. (∀r. P r) ⇔ ∀f b. P <|fld1 := f; fld2 := b|>: thm

> type_vars_in_term (concl it);
val it = [“:β”, “:α”]: hol_type list