# HG changeset patch
# User wenzelm
# Date 1295109127 -3600
# Node ID f5e7f671281520d686f4d4415aad117962d3c021
# Parent  9a64c40078645025005ad14c41099c7e2f9ecd92
recovered printing of record updates over compound terms, e.g. "(|x = a|)(|x := b|)", which was apparently broken in 45a2ffc5911e;
tuned;

diff -r 9a64c4007864 -r f5e7f6712815 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Jan 15 16:49:10 2011 +0100
+++ b/src/HOL/Tools/record.ML	Sat Jan 15 17:32:07 2011 +0100
@@ -953,26 +953,30 @@
 
 local
 
+fun dest_update ctxt c =
+  (case try Syntax.unmark_const c of
+    SOME d => try (unsuffix updateN) (Consts.extern (ProofContext.consts_of ctxt) d)
+  | NONE => NONE);
+
 fun field_updates_tr' ctxt (tm as Const (c, _) $ k $ u) =
-      let
-        val extern = Consts.extern (ProofContext.consts_of ctxt);
-        val t =
-          (case k of
-            Abs (_, _, Abs (_, _, t) $ Bound 0) =>
-              if null (loose_bnos t) then t else raise Match
-          | Abs (_, _, t) =>
-              if null (loose_bnos t) then t else raise Match
-          | _ => raise Match);
-      in
-        (case Option.map extern (try Syntax.unmark_const c) of
-          SOME update_name =>
-            (case try (unsuffix updateN) update_name of
-              SOME name =>
+      (case dest_update ctxt c of
+        SOME name =>
+          let
+            val opt_t =
+              (case k of
+                Abs (_, _, Abs (_, _, t) $ Bound 0) =>
+                  if null (loose_bnos t) then SOME t else NONE
+              | Abs (_, _, t) =>
+                  if null (loose_bnos t) then SOME t else NONE
+              | _ => NONE);
+          in
+            (case opt_t of
+              SOME t =>
                 apfst (cons (Syntax.const @{syntax_const "_field_update"} $ Syntax.free name $ t))
                   (field_updates_tr' ctxt u)
             | NONE => ([], tm))
-        | NONE => ([], tm))
-      end
+          end
+      | NONE => ([], tm))
   | field_updates_tr' _ tm = ([], tm);
 
 fun record_update_tr' ctxt tm =