# HG changeset patch
# User wenzelm
# Date 976561818 -3600
# Node ID d1533f63c73814d414865169952232d91b7c125c
# Parent  562e20e543b10fb283a5774ca846cdab2320b5d4
added "_update_name" and parse_translation;

diff -r 562e20e543b1 -r d1533f63c738 src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon Dec 11 20:09:47 2000 +0100
+++ b/src/HOL/Record.thy	Mon Dec 11 20:10:18 2000 +0100
@@ -35,6 +35,7 @@
   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
 
   (*record updates*)
+  "_update_name"        :: idt
   "_update"             :: "[ident, 'a] => update"                      ("(2_ :=/ _)")
   ""                    :: "update => updates"                          ("_")
   "_updates"            :: "[update, updates] => updates"               ("_,/ _")
@@ -47,6 +48,19 @@
   "_record_scheme"      :: "[fields, 'a] => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   "_record_update"      :: "['a, updates] => 'b"                ("_/(3\<lparr>_\<rparr>)" [900,0] 900)
 
+parse_translation {*
+  let
+    fun update_name_tr (Free (x, T) :: ts) =
+          Term.list_comb (Free (suffix RecordPackage.updateN x, T), ts)
+      | update_name_tr (Const (x, T) :: ts) =
+          Term.list_comb (Const (suffix RecordPackage.updateN x, T), ts)
+      | update_name_tr (((c as Const ("_constrain", _)) $ t $ ty) :: ts) =
+          Term.list_comb (c $ update_name_tr [t] $
+            (Syntax.const "fun" $ ty $ Syntax.const "dummy"), ts)
+      | update_name_tr ts = raise TERM ("update_name_tr", ts);
+  in [("_update_name", update_name_tr)] end
+*}
+
 
 (* type class for record extensions *)