1.1 --- a/src/HOL/Tools/record.ML	Sat Mar 26 10:52:29 2011 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Mar 26 12:01:40 2011 +0100
     1.3 @@ -961,21 +961,11 @@
     1.4  fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
     1.5        (case dest_update ctxt c of
     1.6          SOME name =>
     1.7 -          let
     1.8 -            val opt_t =
     1.9 -              (case k of
    1.10 -                Abs (_, _, Abs (_, _, t) $ Bound 0) =>
    1.11 -                  if null (loose_bnos t) then SOME t else NONE
    1.12 -              | Abs (_, _, t) =>
    1.13 -                  if null (loose_bnos t) then SOME t else NONE
    1.14 -              | _ => NONE);
    1.15 -          in
    1.16 -            (case opt_t of
    1.17 -              SOME t =>
    1.18 -                apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
    1.19 -                  (field_updates_tr' ctxt u)
    1.20 -            | NONE => ([], tm))
    1.21 -          end
    1.22 +          (case try Syntax.const_abs_tr' k of
    1.23 +            SOME t =>
    1.24 +              apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
    1.25 +                (field_updates_tr' ctxt u)
    1.26 +          | NONE => ([], tm))
    1.27        | NONE => ([], tm))
    1.28    | field_updates_tr' _ tm = ([], tm);
    1.29