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

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
```
