src/HOL/Record.thy
changeset 35145 f132a4fd8679
parent 35144 8b8302da3a55
child 35146 f7bf73b0d7e5
--- a/src/HOL/Record.thy	Tue Feb 16 13:35:42 2010 +0100
+++ b/src/HOL/Record.thy	Tue Feb 16 14:08:39 2010 +0100
@@ -437,7 +437,6 @@
   "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
 
-  "_update_name"        :: idt
   "_update"             :: "ident => 'a => update"              ("(2_ :=/ _)")
   ""                    :: "update => updates"                  ("_")
   "_updates"            :: "update => updates => updates"       ("_,/ _")