changeset 42284 | 326f57825e1a |
parent 42247 | 12fe41a92cd5 |
child 42290 | b1f544c84040 |
--- a/src/HOL/Tools/record.ML Fri Apr 08 11:39:45 2011 +0200 +++ b/src/HOL/Tools/record.ML Fri Apr 08 13:31:16 2011 +0200 @@ -963,7 +963,7 @@ fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) = (case dest_update ctxt c of SOME name => - (case try Syntax.const_abs_tr' k of + (case try Syntax_Trans.const_abs_tr' k of SOME t => apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t)) (field_updates_tr' ctxt u)