src/HOL/Tools/record.ML
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)