src/Pure/pure_thy.ML
changeset 35145 f132a4fd8679
parent 35130 0991c84e8dcf
child 35255 2cb27605301f
--- a/src/Pure/pure_thy.ML	Tue Feb 16 13:35:42 2010 +0100
+++ b/src/Pure/pure_thy.ML	Tue Feb 16 14:08:39 2010 +0100
@@ -309,6 +309,7 @@
     ("_indexdefault", typ "index",                     Delimfix ""),
     ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
     ("_struct",     typ "index => logic",              Mixfix ("\\<struct>_", [1000], 1000)),
+    ("_update_name", typ "idt",                        NoSyn),
     ("==>",         typ "prop => prop => prop",        Delimfix "op ==>"),
     (Term.dummy_patternN, typ "aprop",                 Delimfix "'_"),
     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),