src/HOL/Tools/record.ML

       let
         fun mkeq (lr, Teq, (sel, Tsel), x) i =
           if is_selector thy sel then
             let
               val x' =
-                if not (loose_bvar1 (x, 0))
+                if not (Term.is_dependent x)
                 then Free ("x" ^ string_of_int i, range_type Tsel)
                 else raise TERM ("", [x]);
               val sel' = Const (sel, Tsel) $ Bound 0;
               val (l, r) = if lr then (sel', x') else (x', sel');
             in Const (@{const_name HOL.eq}, Teq) $ l $ r end