tuned;

--- a/src/HOL/Tools/record.ML	Fri Mar 30 18:56:46 2012 +0200
+++ b/src/HOL/Tools/record.ML	Fri Mar 30 19:36:41 2012 +0200
@@ -1314,7 +1314,7 @@
           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;