_constify;
authorwenzelm
Wed, 08 Aug 2001 17:38:53 +0200
changeset 11489 1fd5469c195e
parent 11488 4ff900551340
child 11490 f9ae28f55178
_constify;
src/HOL/Record.thy
--- a/src/HOL/Record.thy	Wed Aug 08 17:38:29 2001 +0200
+++ b/src/HOL/Record.thy	Wed Aug 08 17:38:53 2001 +0200
@@ -17,8 +17,8 @@
 
 syntax
   (*field names*)
-  "_field_name"         :: "id => ident"                                ("_")
-  "_field_name"         :: "longid => ident"                            ("_")
+  "_constify"           :: "id => ident"                                ("_")
+  "_constify"           :: "longid => ident"                            ("_")
 
   (*record types*)
   "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")